This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tpostpos

Description: Value of the double transposition for a general class F . (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion tpostpos tpos tpos 𝐹 = ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) )

Proof

Step Hyp Ref Expression
1 reltpos ⊢ Rel tpos tpos 𝐹
2 relinxp ⊢ Rel ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) )
3 relcnv ⊢ Rel ◡ dom tpos 𝐹
4 df-rel ⊢ ( Rel ◡ dom tpos 𝐹 ↔ ◡ dom tpos 𝐹 ⊆ ( V × V ) )
5 3 4 mpbi ⊢ ◡ dom tpos 𝐹 ⊆ ( V × V )
6 simpl ⊢ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) → 𝑤 ∈ ◡ dom tpos 𝐹 )
7 5 6 sselid ⊢ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) → 𝑤 ∈ ( V × V ) )
8 simpr ⊢ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) → 𝑤 ∈ ( V × V ) )
9 elvv ⊢ ( 𝑤 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
10 eleq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ◡ dom tpos 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ dom tpos 𝐹 ) )
11 vex ⊢ 𝑥 ∈ V
12 vex ⊢ 𝑦 ∈ V
13 11 12 opelcnv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ dom tpos 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 )
14 10 13 bitrdi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ◡ dom tpos 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ) )
15 sneq ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑤 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
16 15 cnveqd ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ◡ { 𝑤 } = ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
17 16 unieqd ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ ◡ { 𝑤 } = ∪ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
18 opswap ⊢ ∪ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } = ⟨ 𝑦 , 𝑥 ⟩
19 17 18 eqtrdi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ ◡ { 𝑤 } = ⟨ 𝑦 , 𝑥 ⟩ )
20 19 breq1d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) )
21 14 20 anbi12d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ∧ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) ) )
22 opex ⊢ ⟨ 𝑦 , 𝑥 ⟩ ∈ V
23 vex ⊢ 𝑧 ∈ V
24 22 23 breldm ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 → ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 )
25 24 pm4.71ri ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ∧ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) )
26 brtpos ⊢ ( 𝑧 ∈ V → ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ) )
27 26 elv ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 )
28 25 27 bitr3i ⊢ ( ( ⟨ 𝑦 , 𝑥 ⟩ ∈ dom tpos 𝐹 ∧ ⟨ 𝑦 , 𝑥 ⟩ tpos 𝐹 𝑧 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 )
29 21 28 bitrdi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ) )
30 breq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ) )
31 29 30 bitr4d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ 𝑤 𝐹 𝑧 ) )
32 31 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ 𝑤 𝐹 𝑧 ) )
33 9 32 sylbi ⊢ ( 𝑤 ∈ ( V × V ) → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ 𝑤 𝐹 𝑧 ) )
34 iba ⊢ ( 𝑤 ∈ ( V × V ) → ( 𝑤 𝐹 𝑧 ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ) )
35 33 34 bitrd ⊢ ( 𝑤 ∈ ( V × V ) → ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ) )
36 7 8 35 pm5.21nii ⊢ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) )
37 elsni ⊢ ( 𝑤 ∈ { ∅ } → 𝑤 = ∅ )
38 37 sneqd ⊢ ( 𝑤 ∈ { ∅ } → { 𝑤 } = { ∅ } )
39 38 cnveqd ⊢ ( 𝑤 ∈ { ∅ } → ◡ { 𝑤 } = ◡ { ∅ } )
40 cnvsn0 ⊢ ◡ { ∅ } = ∅
41 39 40 eqtrdi ⊢ ( 𝑤 ∈ { ∅ } → ◡ { 𝑤 } = ∅ )
42 41 unieqd ⊢ ( 𝑤 ∈ { ∅ } → ∪ ◡ { 𝑤 } = ∪ ∅ )
43 uni0 ⊢ ∪ ∅ = ∅
44 42 43 eqtrdi ⊢ ( 𝑤 ∈ { ∅ } → ∪ ◡ { 𝑤 } = ∅ )
45 44 breq1d ⊢ ( 𝑤 ∈ { ∅ } → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ ∅ tpos 𝐹 𝑧 ) )
46 brtpos0 ⊢ ( 𝑧 ∈ V → ( ∅ tpos 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 ) )
47 46 elv ⊢ ( ∅ tpos 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 )
48 45 47 bitrdi ⊢ ( 𝑤 ∈ { ∅ } → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 ) )
49 37 breq1d ⊢ ( 𝑤 ∈ { ∅ } → ( 𝑤 𝐹 𝑧 ↔ ∅ 𝐹 𝑧 ) )
50 48 49 bitr4d ⊢ ( 𝑤 ∈ { ∅ } → ( ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ↔ 𝑤 𝐹 𝑧 ) )
51 50 pm5.32i ⊢ ( ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 ∈ { ∅ } ∧ 𝑤 𝐹 𝑧 ) )
52 51 biancomi ⊢ ( ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ { ∅ } ) )
53 36 52 orbi12i ⊢ ( ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ∨ ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ) ↔ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ∨ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ { ∅ } ) ) )
54 andir ⊢ ( ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ∨ ( 𝑤 ∈ { ∅ } ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ) )
55 andi ⊢ ( ( 𝑤 𝐹 𝑧 ∧ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) ) ↔ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ ( V × V ) ) ∨ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ∈ { ∅ } ) ) )
56 53 54 55 3bitr4i ⊢ ( ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) ) )
57 elun ⊢ ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ↔ ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) )
58 57 anbi1i ⊢ ( ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( ( 𝑤 ∈ ◡ dom tpos 𝐹 ∨ 𝑤 ∈ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) )
59 brxp ⊢ ( 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ↔ ( 𝑤 ∈ ( ( V × V ) ∪ { ∅ } ) ∧ 𝑧 ∈ V ) )
60 23 59 mpbiran2 ⊢ ( 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ↔ 𝑤 ∈ ( ( V × V ) ∪ { ∅ } ) )
61 elun ⊢ ( 𝑤 ∈ ( ( V × V ) ∪ { ∅ } ) ↔ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) )
62 60 61 bitri ⊢ ( 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ↔ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) )
63 62 anbi2i ⊢ ( ( 𝑤 𝐹 𝑧 ∧ 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ ( 𝑤 ∈ ( V × V ) ∨ 𝑤 ∈ { ∅ } ) ) )
64 56 58 63 3bitr4i ⊢ ( ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ) )
65 brtpos2 ⊢ ( 𝑧 ∈ V → ( 𝑤 tpos tpos 𝐹 𝑧 ↔ ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) ) )
66 65 elv ⊢ ( 𝑤 tpos tpos 𝐹 𝑧 ↔ ( 𝑤 ∈ ( ◡ dom tpos 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { 𝑤 } tpos 𝐹 𝑧 ) )
67 brin ⊢ ( 𝑤 ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) ) 𝑧 ↔ ( 𝑤 𝐹 𝑧 ∧ 𝑤 ( ( ( V × V ) ∪ { ∅ } ) × V ) 𝑧 ) )
68 64 66 67 3bitr4i ⊢ ( 𝑤 tpos tpos 𝐹 𝑧 ↔ 𝑤 ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) ) 𝑧 )
69 1 2 68 eqbrriv ⊢ tpos tpos 𝐹 = ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) )