Metamath Proof Explorer

Theorem dftpos4

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

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

Proof

Step Hyp Ref Expression
1 df-tpos ⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
2 relcnv ⊢ Rel ◡ dom 𝐹
3 df-rel ⊢ ( Rel ◡ dom 𝐹 ↔ ◡ dom 𝐹 ⊆ ( V × V ) )
4 2 3 mpbi ⊢ ◡ dom 𝐹 ⊆ ( V × V )
5 unss1 ⊢ ( ◡ dom 𝐹 ⊆ ( V × V ) → ( ◡ dom 𝐹 ∪ { ∅ } ) ⊆ ( ( V × V ) ∪ { ∅ } ) )
6 resmpt ⊢ ( ( ◡ dom 𝐹 ∪ { ∅ } ) ⊆ ( ( V × V ) ∪ { ∅ } ) → ( ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↾ ( ◡ dom 𝐹 ∪ { ∅ } ) ) = ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
7 4 5 6 mp2b ⊢ ( ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↾ ( ◡ dom 𝐹 ∪ { ∅ } ) ) = ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
8 resss ⊢ ( ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↾ ( ◡ dom 𝐹 ∪ { ∅ } ) ) ⊆ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
9 7 8 eqsstrri ⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
10 coss2 ⊢ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) → ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ⊆ ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) )
11 9 10 ax-mp ⊢ ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ⊆ ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
12 1 11 eqsstri ⊢ tpos 𝐹 ⊆ ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
13 relco ⊢ Rel ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
14 vex ⊢ 𝑦 ∈ V
15 vex ⊢ 𝑧 ∈ V
16 14 15 opelco ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ↔ ∃ 𝑤 ( 𝑦 ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑤 ∧ 𝑤 𝐹 𝑧 ) )
17 vex ⊢ 𝑤 ∈ V
18 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↔ 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ) )
19 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
20 19 cnveqd ⊢ ( 𝑥 = 𝑦 → ◡ { 𝑥 } = ◡ { 𝑦 } )
21 20 unieqd ⊢ ( 𝑥 = 𝑦 → ∪ ◡ { 𝑥 } = ∪ ◡ { 𝑦 } )
22 21 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑧 = ∪ ◡ { 𝑥 } ↔ 𝑧 = ∪ ◡ { 𝑦 } ) )
23 18 22 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑧 = ∪ ◡ { 𝑥 } ) ↔ ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑧 = ∪ ◡ { 𝑦 } ) ) )
24 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ∪ ◡ { 𝑦 } ↔ 𝑤 = ∪ ◡ { 𝑦 } ) )
25 24 anbi2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑧 = ∪ ◡ { 𝑦 } ) ↔ ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ) )
26 df-mpt ⊢ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑧 = ∪ ◡ { 𝑥 } ) }
27 14 17 23 25 26 brab ⊢ ( 𝑦 ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑤 ↔ ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) )
28 simplr ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → 𝑤 = ∪ ◡ { 𝑦 } )
29 17 15 breldm ⊢ ( 𝑤 𝐹 𝑧 → 𝑤 ∈ dom 𝐹 )
30 29 adantl ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → 𝑤 ∈ dom 𝐹 )
31 28 30 eqeltrrd ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → ∪ ◡ { 𝑦 } ∈ dom 𝐹 )
32 elvv ⊢ ( 𝑦 ∈ ( V × V ) ↔ ∃ 𝑧 ∃ 𝑤 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ )
33 opswap ⊢ ∪ ◡ { ⟨ 𝑧 , 𝑤 ⟩ } = ⟨ 𝑤 , 𝑧 ⟩
34 33 eleq1i ⊢ ( ∪ ◡ { ⟨ 𝑧 , 𝑤 ⟩ } ∈ dom 𝐹 ↔ ⟨ 𝑤 , 𝑧 ⟩ ∈ dom 𝐹 )
35 15 17 opelcnv ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ◡ dom 𝐹 ↔ ⟨ 𝑤 , 𝑧 ⟩ ∈ dom 𝐹 )
36 34 35 bitr4i ⊢ ( ∪ ◡ { ⟨ 𝑧 , 𝑤 ⟩ } ∈ dom 𝐹 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ◡ dom 𝐹 )
37 sneq ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → { 𝑦 } = { ⟨ 𝑧 , 𝑤 ⟩ } )
38 37 cnveqd ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ◡ { 𝑦 } = ◡ { ⟨ 𝑧 , 𝑤 ⟩ } )
39 38 unieqd ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ∪ ◡ { 𝑦 } = ∪ ◡ { ⟨ 𝑧 , 𝑤 ⟩ } )
40 39 eleq1d ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∪ ◡ { 𝑦 } ∈ dom 𝐹 ↔ ∪ ◡ { ⟨ 𝑧 , 𝑤 ⟩ } ∈ dom 𝐹 ) )
41 eleq1 ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑦 ∈ ◡ dom 𝐹 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ◡ dom 𝐹 ) )
42 40 41 bibi12d ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( ∪ ◡ { 𝑦 } ∈ dom 𝐹 ↔ 𝑦 ∈ ◡ dom 𝐹 ) ↔ ( ∪ ◡ { ⟨ 𝑧 , 𝑤 ⟩ } ∈ dom 𝐹 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ◡ dom 𝐹 ) ) )
43 36 42 mpbiri ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∪ ◡ { 𝑦 } ∈ dom 𝐹 ↔ 𝑦 ∈ ◡ dom 𝐹 ) )
44 43 exlimivv ⊢ ( ∃ 𝑧 ∃ 𝑤 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∪ ◡ { 𝑦 } ∈ dom 𝐹 ↔ 𝑦 ∈ ◡ dom 𝐹 ) )
45 32 44 sylbi ⊢ ( 𝑦 ∈ ( V × V ) → ( ∪ ◡ { 𝑦 } ∈ dom 𝐹 ↔ 𝑦 ∈ ◡ dom 𝐹 ) )
46 45 biimpcd ⊢ ( ∪ ◡ { 𝑦 } ∈ dom 𝐹 → ( 𝑦 ∈ ( V × V ) → 𝑦 ∈ ◡ dom 𝐹 ) )
47 elun1 ⊢ ( 𝑦 ∈ ◡ dom 𝐹 → 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) )
48 46 47 syl6 ⊢ ( ∪ ◡ { 𝑦 } ∈ dom 𝐹 → ( 𝑦 ∈ ( V × V ) → 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) )
49 31 48 syl ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → ( 𝑦 ∈ ( V × V ) → 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) )
50 elun2 ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) )
51 50 a1i ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → ( 𝑦 ∈ { ∅ } → 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) )
52 simpll ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) )
53 elun ⊢ ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ↔ ( 𝑦 ∈ ( V × V ) ∨ 𝑦 ∈ { ∅ } ) )
54 52 53 sylib ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → ( 𝑦 ∈ ( V × V ) ∨ 𝑦 ∈ { ∅ } ) )
55 49 51 54 mpjaod ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) )
56 simpr ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → 𝑤 𝐹 𝑧 )
57 28 56 eqbrtrrd ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → ∪ ◡ { 𝑦 } 𝐹 𝑧 )
58 55 57 jca ⊢ ( ( ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑤 = ∪ ◡ { 𝑦 } ) ∧ 𝑤 𝐹 𝑧 ) → ( 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑦 } 𝐹 𝑧 ) )
59 27 58 sylanb ⊢ ( ( 𝑦 ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑤 ∧ 𝑤 𝐹 𝑧 ) → ( 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑦 } 𝐹 𝑧 ) )
60 brtpos2 ⊢ ( 𝑧 ∈ V → ( 𝑦 tpos 𝐹 𝑧 ↔ ( 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑦 } 𝐹 𝑧 ) ) )
61 15 60 ax-mp ⊢ ( 𝑦 tpos 𝐹 𝑧 ↔ ( 𝑦 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑦 } 𝐹 𝑧 ) )
62 59 61 sylibr ⊢ ( ( 𝑦 ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑤 ∧ 𝑤 𝐹 𝑧 ) → 𝑦 tpos 𝐹 𝑧 )
63 df-br ⊢ ( 𝑦 tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ tpos 𝐹 )
64 62 63 sylib ⊢ ( ( 𝑦 ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑤 ∧ 𝑤 𝐹 𝑧 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ tpos 𝐹 )
65 64 exlimiv ⊢ ( ∃ 𝑤 ( 𝑦 ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) 𝑤 ∧ 𝑤 𝐹 𝑧 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ tpos 𝐹 )
66 16 65 sylbi ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ tpos 𝐹 )
67 13 66 relssi ⊢ ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ⊆ tpos 𝐹
68 12 67 eqssi ⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )