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 F = F ∩ V × V ∪ ∅ × V

Proof

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