Theorem dftpos4 8220

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 8201	. . 3 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
2		relcnv 6090	. . . . . . 7 ⊢ Rel ◡dom 𝐹
3		df-rel 5652	. . . . . . 7 ⊢ (Rel ◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V))
4	2, 3	mpbi 232	. . . . . 6 ⊢ ◡dom 𝐹 ⊆ (V × V)
5		unss1 4137	. . . . . 6 ⊢ (◡dom 𝐹 ⊆ (V × V) → (◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}))
6		resmpt 6023	. . . . . 6 ⊢ ((◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}) → ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
7	4, 5, 6	mp2b 10	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})
8		resss 5985	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
9	7, 8	eqsstrri 3983	. . . 4 ⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
10		coss2 5826	. . . 4 ⊢ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) → (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})))
11	9, 10	ax-mp 5	. . 3 ⊢ (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
12	1, 11	eqsstri 3982	. 2 ⊢ tpos 𝐹 ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
13		relco 6094	. . 3 ⊢ Rel (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
14		vex 3457	. . . . 5 ⊢ 𝑦 ∈ V
15		vex 3457	. . . . 5 ⊢ 𝑧 ∈ V
16	14, 15	opelco 5841	. . . 4 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ↔ ∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧))
17		vex 3457	. . . . . . . . 9 ⊢ 𝑤 ∈ V
18		eleq1 2849	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ((V × V) ∪ {∅}) ↔ 𝑦 ∈ ((V × V) ∪ {∅})))
19		sneq 4591	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
20	19	cnveqd 5845	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ◡{𝑥} = ◡{𝑦})
21	20	unieqd 4877	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ∪ ◡{𝑥} = ∪ ◡{𝑦})
22	21	eqeq2d 2772	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑧 = ∪ ◡{𝑥} ↔ 𝑧 = ∪ ◡{𝑦}))
23	18, 22	anbi12d 641	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦})))
24		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (𝑧 = ∪ ◡{𝑦} ↔ 𝑤 = ∪ ◡{𝑦}))
25	24	anbi2d 639	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦})))
26		df-mpt 5181	. . . . . . . . 9 ⊢ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥})}
27	14, 17, 23, 25, 26	brab 5512	. . . . . . . 8 ⊢ (𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}))
28		simplr 778	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 = ∪ ◡{𝑦})
29	17, 15	breldm 5882	. . . . . . . . . . . . 13 ⊢ (𝑤𝐹𝑧 → 𝑤 ∈ dom 𝐹)
30	29	adantl 485	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 ∈ dom 𝐹)
31	28, 30	eqeltrrd 2862	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦} ∈ dom 𝐹)
32		elvv 5720	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (V × V) ↔ ∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩)
33		opswap 6212	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩
34	33	eleq1i 2852	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
35	15, 17	opelcnv 5851	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
36	34, 35	bitr4i 280	. . . . . . . . . . . . . . . 16 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)
37		sneq 4591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → {𝑦} = {⟨𝑧, 𝑤⟩})
38	37	cnveqd 5845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ◡{𝑦} = ◡{⟨𝑧, 𝑤⟩})
39	38	unieqd 4877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ∪ ◡{𝑦} = ∪ ◡{⟨𝑧, 𝑤⟩})
40	39	eleq1d 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ ∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹))
41		eleq1 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ◡dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹))
42	40, 41	bibi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ((∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹) ↔ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)))
43	36, 42	mpbiri 260	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
44	43	exlimivv 1951	. . . . . . . . . . . . . 14 ⊢ (∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
45	32, 44	sylbi 219	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (V × V) → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
46	45	biimpcd 251	. . . . . . . . . . . 12 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ ◡dom 𝐹))
47		elun1 4134	. . . . . . . . . . . 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 4135	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
51	50	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
52		simpll 776	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ ((V × V) ∪ {∅}))
53		elun 4106	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((V × V) ∪ {∅}) ↔ (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
54	52, 53	sylib 220	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
55	49, 51, 54	mpjaod 871	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
56		simpr 488	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤𝐹𝑧)
57	28, 56	eqbrtrrd 5123	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦}𝐹𝑧)
58	55, 57	jca 519	. . . . . . . 8 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
59	27, 58	sylanb 590	. . . . . . 7 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
60		brtpos2 8207	. . . . . . . 8 ⊢ (𝑧 ∈ V → (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)))
61	15, 60	ax-mp 5	. . . . . . 7 ⊢ (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
62	59, 61	sylibr 236	. . . . . 6 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → 𝑦tpos 𝐹𝑧)
63		df-br 5100	. . . . . 6 ⊢ (𝑦tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
64	62, 63	sylib 220	. . . . 5 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
65	64	exlimiv 1949	. . . 4 ⊢ (∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
66	16, 65	sylbi 219	. . 3 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
67	13, 66	relssi 5757	. 2 ⊢ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ tpos 𝐹
68	12, 67	eqssi 3952	1 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1559  ∃wex 1798   ∈ wcel 2141  Vcvv 3453   ∪ cun 3902   ⊆ wss 3904  ∅c0 4285  {csn 4581  ⟨cop 4587  ∪ cuni 4864   class class class wbr 5099   ↦ cmpt 5180   × cxp 5643  ^◡ccnv 5644  dom cdm 5645   ↾ cres 5647   ∘ ccom 5649  Rel wrel 5650  tpos ctpos 8200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-fv 6525  df-tpos 8201

This theorem is referenced by:  tposco  8232  nftpos  8236  oftpos  22492