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 ) )