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 ⊢ ( 𝐺 ∘ 𝐹 ) = ( 𝑧 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )