Metamath Proof Explorer


Theorem xpcomco

Description: Composition with the bijection of xpcomf1o swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses xpcomf1o.1 𝐹 = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } )
xpcomco.1 𝐺 = ( 𝑦𝐵 , 𝑧𝐴𝐶 )
Assertion xpcomco ( 𝐺𝐹 ) = ( 𝑧𝐴 , 𝑦𝐵𝐶 )

Proof

Step Hyp Ref Expression
1 xpcomf1o.1 𝐹 = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ { 𝑥 } )
2 xpcomco.1 𝐺 = ( 𝑦𝐵 , 𝑧𝐴𝐶 )
3 1 xpcomf1o 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 )
4 f1ofun ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) → Fun 𝐹 )
5 funbrfv2b ( Fun 𝐹 → ( 𝑢 𝐹 𝑤 ↔ ( 𝑢 ∈ dom 𝐹 ∧ ( 𝐹𝑢 ) = 𝑤 ) ) )
6 3 4 5 mp2b ( 𝑢 𝐹 𝑤 ↔ ( 𝑢 ∈ dom 𝐹 ∧ ( 𝐹𝑢 ) = 𝑤 ) )
7 ancom ( ( 𝑢 ∈ dom 𝐹 ∧ ( 𝐹𝑢 ) = 𝑤 ) ↔ ( ( 𝐹𝑢 ) = 𝑤𝑢 ∈ dom 𝐹 ) )
8 eqcom ( ( 𝐹𝑢 ) = 𝑤𝑤 = ( 𝐹𝑢 ) )
9 f1odm ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) → dom 𝐹 = ( 𝐴 × 𝐵 ) )
10 3 9 ax-mp dom 𝐹 = ( 𝐴 × 𝐵 )
11 10 eleq2i ( 𝑢 ∈ dom 𝐹𝑢 ∈ ( 𝐴 × 𝐵 ) )
12 8 11 anbi12i ( ( ( 𝐹𝑢 ) = 𝑤𝑢 ∈ dom 𝐹 ) ↔ ( 𝑤 = ( 𝐹𝑢 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) )
13 6 7 12 3bitri ( 𝑢 𝐹 𝑤 ↔ ( 𝑤 = ( 𝐹𝑢 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) )
14 13 anbi1i ( ( 𝑢 𝐹 𝑤𝑤 𝐺 𝑣 ) ↔ ( ( 𝑤 = ( 𝐹𝑢 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) ∧ 𝑤 𝐺 𝑣 ) )
15 anass ( ( ( 𝑤 = ( 𝐹𝑢 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) ∧ 𝑤 𝐺 𝑣 ) ↔ ( 𝑤 = ( 𝐹𝑢 ) ∧ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 𝐺 𝑣 ) ) )
16 14 15 bitri ( ( 𝑢 𝐹 𝑤𝑤 𝐺 𝑣 ) ↔ ( 𝑤 = ( 𝐹𝑢 ) ∧ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 𝐺 𝑣 ) ) )
17 16 exbii ( ∃ 𝑤 ( 𝑢 𝐹 𝑤𝑤 𝐺 𝑣 ) ↔ ∃ 𝑤 ( 𝑤 = ( 𝐹𝑢 ) ∧ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 𝐺 𝑣 ) ) )
18 fvex ( 𝐹𝑢 ) ∈ V
19 breq1 ( 𝑤 = ( 𝐹𝑢 ) → ( 𝑤 𝐺 𝑣 ↔ ( 𝐹𝑢 ) 𝐺 𝑣 ) )
20 19 anbi2d ( 𝑤 = ( 𝐹𝑢 ) → ( ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 𝐺 𝑣 ) ↔ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ) )
21 18 20 ceqsexv ( ∃ 𝑤 ( 𝑤 = ( 𝐹𝑢 ) ∧ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑤 𝐺 𝑣 ) ) ↔ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) )
22 elxp ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) )
23 22 anbi1i ( ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ( ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) )
24 nfcv 𝑧 ( 𝐹𝑢 )
25 nfmpo2 𝑧 ( 𝑦𝐵 , 𝑧𝐴𝐶 )
26 2 25 nfcxfr 𝑧 𝐺
27 nfcv 𝑧 𝑣
28 24 26 27 nfbr 𝑧 ( 𝐹𝑢 ) 𝐺 𝑣
29 28 19.41 ( ∃ 𝑧 ( ∃ 𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ( ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) )
30 nfcv 𝑦 ( 𝐹𝑢 )
31 nfmpo1 𝑦 ( 𝑦𝐵 , 𝑧𝐴𝐶 )
32 2 31 nfcxfr 𝑦 𝐺
33 nfcv 𝑦 𝑣
34 30 32 33 nfbr 𝑦 ( 𝐹𝑢 ) 𝐺 𝑣
35 34 19.41 ( ∃ 𝑦 ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ( ∃ 𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) )
36 anass ( ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ) )
37 fveq2 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ → ( 𝐹𝑢 ) = ( 𝐹 ‘ ⟨ 𝑧 , 𝑦 ⟩ ) )
38 opelxpi ( ( 𝑧𝐴𝑦𝐵 ) → ⟨ 𝑧 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
39 sneq ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ → { 𝑥 } = { ⟨ 𝑧 , 𝑦 ⟩ } )
40 39 cnveqd ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ → { 𝑥 } = { ⟨ 𝑧 , 𝑦 ⟩ } )
41 40 unieqd ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ → { 𝑥 } = { ⟨ 𝑧 , 𝑦 ⟩ } )
42 opswap { ⟨ 𝑧 , 𝑦 ⟩ } = ⟨ 𝑦 , 𝑧
43 41 42 eqtrdi ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ → { 𝑥 } = ⟨ 𝑦 , 𝑧 ⟩ )
44 opex 𝑦 , 𝑧 ⟩ ∈ V
45 43 1 44 fvmpt ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ( 𝐹 ‘ ⟨ 𝑧 , 𝑦 ⟩ ) = ⟨ 𝑦 , 𝑧 ⟩ )
46 38 45 syl ( ( 𝑧𝐴𝑦𝐵 ) → ( 𝐹 ‘ ⟨ 𝑧 , 𝑦 ⟩ ) = ⟨ 𝑦 , 𝑧 ⟩ )
47 37 46 sylan9eq ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) → ( 𝐹𝑢 ) = ⟨ 𝑦 , 𝑧 ⟩ )
48 47 breq1d ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) → ( ( 𝐹𝑢 ) 𝐺 𝑣 ↔ ⟨ 𝑦 , 𝑧𝐺 𝑣 ) )
49 df-br ( ⟨ 𝑦 , 𝑧𝐺 𝑣 ↔ ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∈ 𝐺 )
50 df-mpo ( 𝑦𝐵 , 𝑧𝐴𝐶 ) = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑦𝐵𝑧𝐴 ) ∧ 𝑣 = 𝐶 ) }
51 2 50 eqtri 𝐺 = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑦𝐵𝑧𝐴 ) ∧ 𝑣 = 𝐶 ) }
52 51 eleq2i ( ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∈ 𝐺 ↔ ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∈ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑦𝐵𝑧𝐴 ) ∧ 𝑣 = 𝐶 ) } )
53 oprabidw ( ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∈ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑦𝐵𝑧𝐴 ) ∧ 𝑣 = 𝐶 ) } ↔ ( ( 𝑦𝐵𝑧𝐴 ) ∧ 𝑣 = 𝐶 ) )
54 49 52 53 3bitri ( ⟨ 𝑦 , 𝑧𝐺 𝑣 ↔ ( ( 𝑦𝐵𝑧𝐴 ) ∧ 𝑣 = 𝐶 ) )
55 54 baib ( ( 𝑦𝐵𝑧𝐴 ) → ( ⟨ 𝑦 , 𝑧𝐺 𝑣𝑣 = 𝐶 ) )
56 55 ancoms ( ( 𝑧𝐴𝑦𝐵 ) → ( ⟨ 𝑦 , 𝑧𝐺 𝑣𝑣 = 𝐶 ) )
57 56 adantl ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) → ( ⟨ 𝑦 , 𝑧𝐺 𝑣𝑣 = 𝐶 ) )
58 48 57 bitrd ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) → ( ( 𝐹𝑢 ) 𝐺 𝑣𝑣 = 𝐶 ) )
59 58 pm5.32da ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ → ( ( ( 𝑧𝐴𝑦𝐵 ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
60 59 pm5.32i ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ) ↔ ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
61 36 60 bitri ( ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
62 61 exbii ( ∃ 𝑦 ( ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ∃ 𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
63 35 62 bitr3i ( ( ∃ 𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ∃ 𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
64 63 exbii ( ∃ 𝑧 ( ∃ 𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( 𝑧𝐴𝑦𝐵 ) ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
65 23 29 64 3bitr2i ( ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝐹𝑢 ) 𝐺 𝑣 ) ↔ ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
66 17 21 65 3bitri ( ∃ 𝑤 ( 𝑢 𝐹 𝑤𝑤 𝐺 𝑣 ) ↔ ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) )
67 66 opabbii { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑤 ( 𝑢 𝐹 𝑤𝑤 𝐺 𝑣 ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) }
68 df-co ( 𝐺𝐹 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑤 ( 𝑢 𝐹 𝑤𝑤 𝐺 𝑣 ) }
69 df-mpo ( 𝑧𝐴 , 𝑦𝐵𝐶 ) = { ⟨ ⟨ 𝑧 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) }
70 dfoprab2 { ⟨ ⟨ 𝑧 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) }
71 69 70 eqtri ( 𝑧𝐴 , 𝑦𝐵𝐶 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑧𝑦 ( 𝑢 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ( ( 𝑧𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ) }
72 67 68 71 3eqtr4i ( 𝐺𝐹 ) = ( 𝑧𝐴 , 𝑦𝐵𝐶 )