Theorem dftpos4 6258

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 6240	. . 3 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
2		relcnv 5002	. . . . . . 7 ⊢ Rel ◡dom 𝐹
3		df-rel 4630	. . . . . . 7 ⊢ (Rel ◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V))
4	2, 3	mpbi 145	. . . . . 6 ⊢ ◡dom 𝐹 ⊆ (V × V)
5		unss1 3304	. . . . . 6 ⊢ (◡dom 𝐹 ⊆ (V × V) → (◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}))
6		resmpt 4951	. . . . . 6 ⊢ ((◡dom 𝐹 ∪ {∅}) ⊆ ((V × V) ∪ {∅}) → ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
7	4, 5, 6	mp2b 8	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})
8		resss 4927	. . . . 5 ⊢ ((𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
9	7, 8	eqsstrri 3188	. . . 4 ⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})
10		coss2 4779	. . . 4 ⊢ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) → (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})))
11	9, 10	ax-mp 5	. . 3 ⊢ (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
12	1, 11	eqsstri 3187	. 2 ⊢ tpos 𝐹 ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
13		relco 5123	. . 3 ⊢ Rel (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
14		vex 2740	. . . . 5 ⊢ 𝑦 ∈ V
15		vex 2740	. . . . 5 ⊢ 𝑧 ∈ V
16	14, 15	opelco 4795	. . . 4 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ↔ ∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧))
17		vex 2740	. . . . . . . . 9 ⊢ 𝑤 ∈ V
18		eleq1 2240	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ((V × V) ∪ {∅}) ↔ 𝑦 ∈ ((V × V) ∪ {∅})))
19		sneq 3602	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
20	19	cnveqd 4799	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ◡{𝑥} = ◡{𝑦})
21	20	unieqd 3818	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ∪ ◡{𝑥} = ∪ ◡{𝑦})
22	21	eqeq2d 2189	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑧 = ∪ ◡{𝑥} ↔ 𝑧 = ∪ ◡{𝑦}))
23	18, 22	anbi12d 473	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦})))
24		eqeq1 2184	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (𝑧 = ∪ ◡{𝑦} ↔ 𝑤 = ∪ ◡{𝑦}))
25	24	anbi2d 464	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑦}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦})))
26		df-mpt 4063	. . . . . . . . 9 ⊢ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ((V × V) ∪ {∅}) ∧ 𝑧 = ∪ ◡{𝑥})}
27	14, 17, 23, 25, 26	brab 4269	. . . . . . . 8 ⊢ (𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}))
28		simplr 528	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 = ∪ ◡{𝑦})
29	17, 15	breldm 4827	. . . . . . . . . . . . 13 ⊢ (𝑤𝐹𝑧 → 𝑤 ∈ dom 𝐹)
30	29	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 ∈ dom 𝐹)
31	28, 30	eqeltrrd 2255	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦} ∈ dom 𝐹)
32		elvv 4685	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (V × V) ↔ ∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩)
33		opswapg 5111	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V) → ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩)
34	15, 17, 33	mp2an 426	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩
35	34	eleq1i 2243	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
36	15, 17	opelcnv 4805	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹)
37	35, 36	bitr4i 187	. . . . . . . . . . . . . . . 16 ⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)
38		sneq 3602	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → {𝑦} = {⟨𝑧, 𝑤⟩})
39	38	cnveqd 4799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ◡{𝑦} = ◡{⟨𝑧, 𝑤⟩})
40	39	unieqd 3818	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ∪ ◡{𝑦} = ∪ ◡{⟨𝑧, 𝑤⟩})
41	40	eleq1d 2246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ ∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹))
42		eleq1 2240	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ◡dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹))
43	41, 42	bibi12d 235	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ((∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹) ↔ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)))
44	37, 43	mpbiri 168	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
45	44	exlimivv 1896	. . . . . . . . . . . . . 14 ⊢ (∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
46	32, 45	sylbi 121	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (V × V) → (∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹))
47	46	biimpcd 159	. . . . . . . . . . . 12 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ ◡dom 𝐹))
48		elun1 3302	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ◡dom 𝐹 → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
49	47, 48	syl6 33	. . . . . . . . . . 11 ⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
50	31, 49	syl 14	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
51		elun2 3303	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
52	51	a1i 9	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})))
53		simpll 527	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ ((V × V) ∪ {∅}))
54		elun 3276	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((V × V) ∪ {∅}) ↔ (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
55	53, 54	sylib 122	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅}))
56	50, 52, 55	mpjaod 718	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))
57		simpr 110	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤𝐹𝑧)
58	28, 57	eqbrtrrd 4024	. . . . . . . . 9 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦}𝐹𝑧)
59	56, 58	jca 306	. . . . . . . 8 ⊢ (((𝑦 ∈ ((V × V) ∪ {∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
60	27, 59	sylanb 284	. . . . . . 7 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
61		brtpos2 6246	. . . . . . . 8 ⊢ (𝑧 ∈ V → (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)))
62	15, 61	ax-mp 5	. . . . . . 7 ⊢ (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))
63	60, 62	sylibr 134	. . . . . 6 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → 𝑦tpos 𝐹𝑧)
64		df-br 4001	. . . . . 6 ⊢ (𝑦tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
65	63, 64	sylib 122	. . . . 5 ⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
66	65	exlimiv 1598	. . . 4 ⊢ (∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
67	16, 66	sylbi 121	. . 3 ⊢ (⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹)
68	13, 67	relssi 4714	. 2 ⊢ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ tpos 𝐹
69	12, 68	eqssi 3171	1 ⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708   = wceq 1353  ∃wex 1492   ∈ wcel 2148  Vcvv 2737   ∪ cun 3127   ⊆ wss 3129  ∅c0 3422  {csn 3591  ⟨cop 3594  ∪ cuni 3807   class class class wbr 4000   ↦ cmpt 4061   × cxp 4621  ^◡ccnv 4622  dom cdm 4623   ↾ cres 4625   ∘ ccom 4627  Rel wrel 4628  tpos ctpos 6239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-fv 5220  df-tpos 6240

This theorem is referenced by:  tposco  6270  nftpos  6274