Theorem dftpos4 7371

Description: Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)

Assertion

Ref	Expression
dftpos4	⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))

Distinct variable group:   𝑥,𝐹

Proof of Theorem dftpos4

Dummy variables 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-tpos 7352	. . 3 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
2		relcnv 5503	. . . . . . 7 ⊢ Rel ◡dom 𝐹
3		df-rel 5121	. . . . . . 7 ⊢ (Rel ◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V))
4	2, 3	mpbi 220	. . . . . 6 ⊢ ◡dom 𝐹 ⊆ (V × V)
5		unss1 3782	. . . . . 6 ⊢ (◡dom 𝐹 ⊆ (V × V) → (◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}))
6		resmpt 5449	. . . . . 6 ⊢ ((◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}) → ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
7	4, 5, 6	mp2b 10	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})
8		resss 5422	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
9	7, 8	eqsstr3i 3636	. . . 4 ⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
10		coss2 5278	. . . 4 ⊢ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) → (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})))
11	9, 10	ax-mp 5	. . 3 ⊢ (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
12	1, 11	eqsstri 3635	. 2 ⊢ tpos 𝐹 ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
13		relco 5633	. . 3 ⊢ Rel (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
14		vex 3203	. . . . 5 ⊢ 𝑦 ∈ V
15		vex 3203	. . . . 5 ⊢ 𝑧 ∈ V
16	14, 15	opelco 5293	. . . 4 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ↔ ∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧))
17		vex 3203	. . . . . . . . 9 ⊢ 𝑤 ∈ V
18		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ((V × V) ∪ {∅}) ↔ 𝑦 ∈ ((V × V) ∪ {∅})))
19		sneq 4187	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
20	19	cnveqd 5298	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ◡{𝑥} = ◡{𝑦})
21	20	unieqd 4446	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ∪ ◡{𝑥} = ∪ ◡{𝑦})
22	21	eqeq2d 2632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑧 = ∪ ◡{𝑥} ↔ 𝑧 = ∪ ◡{𝑦}))
23	18, 22	anbi12d 747	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦})))
24		eqeq1 2626	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (𝑧 = ∪ ◡{𝑦} ↔ 𝑤 = ∪ ◡{𝑦}))
25	24	anbi2d 740	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦})))
26		df-mpt 4730	. . . . . . . . 9 ⊢ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥})}
27	14, 17, 23, 25, 26	brab 4998	. . . . . . . 8 ⊢ (𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}))
28		simplr 792	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 = ∪ ◡{𝑦})
29	17, 15	breldm 5329	. . . . . . . . . . . . 13 ⊢ (𝑤𝐹𝑧 → 𝑤 ∈ dom 𝐹)
30	29	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 ∈ dom 𝐹)
31	28, 30	eqeltrrd 2702	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦} ∈ dom 𝐹)
32		elvv 5177	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (V × V) ↔ ∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩)
33		opswap 5622	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩
34	33	eleq1i 2692	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
35	15, 17	opelcnv 5304	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
36	34, 35	bitr4i 267	. . . . . . . . . . . . . . . 16 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)
37		sneq 4187	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → {𝑦} = {⟨𝑧, 𝑤⟩})
38	37	cnveqd 5298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ◡{𝑦} = ◡{⟨𝑧, 𝑤⟩})
39	38	unieqd 4446	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ∪ ◡{𝑦} = ∪ ◡{⟨𝑧, 𝑤⟩})
40	39	eleq1d 2686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ ∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹))
41		eleq1 2689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ◡dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹))
42	40, 41	bibi12d 335	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ((∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹) ↔ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)))
43	36, 42	mpbiri 248	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
44	43	exlimivv 1860	. . . . . . . . . . . . . 14 ⊢ (∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
45	32, 44	sylbi 207	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (V × V) → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
46	45	biimpcd 239	. . . . . . . . . . . 12 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ ◡dom 𝐹))
47		elun1 3780	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ◡dom 𝐹 → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
48	46, 47	syl6 35	. . . . . . . . . . 11 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
49	31, 48	syl 17	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
50		elun2 3781	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
51	50	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
52		simpll 790	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ ((V × V) ∪ {∅}))
53		elun 3753	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((V × V) ∪ {∅}) ↔ (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
54	52, 53	sylib 208	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
55	49, 51, 54	mpjaod 396	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
56		simpr 477	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤𝐹𝑧)
57	28, 56	eqbrtrrd 4677	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦}𝐹𝑧)
58	55, 57	jca 554	. . . . . . . 8 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
59	27, 58	sylanb 489	. . . . . . 7 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
60		brtpos2 7358	. . . . . . . 8 ⊢ (𝑧 ∈ V → (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)))
61	15, 60	ax-mp 5	. . . . . . 7 ⊢ (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
62	59, 61	sylibr 224	. . . . . 6 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → 𝑦tpos 𝐹𝑧)
63		df-br 4654	. . . . . 6 ⊢ (𝑦tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
64	62, 63	sylib 208	. . . . 5 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
65	64	exlimiv 1858	. . . 4 ⊢ (∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
66	16, 65	sylbi 207	. . 3 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
67	13, 66	relssi 5211	. 2 ⊢ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ tpos 𝐹
68	12, 67	eqssi 3619	1 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572   ⊆ wss 3574  ∅c0 3915  {csn 4177  ⟨cop 4183  ∪ cuni 4436   class class class wbr 4653   ↦ cmpt 4729   × cxp 5112  ^◡ccnv 5113  dom cdm 5114   ↾ cres 5116   ∘ ccom 5118  Rel wrel 5119  tpos ctpos 7351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-tpos 7352

This theorem is referenced by:  tposco  7383  nftpos  7387  oftpos  20258