Metamath Proof Explorer

Theorem xpf1o

Description: Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses xpf1o.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 –1-1-onto→ 𝐵 )
xpf1o.2 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑌 ) : 𝐶 –1-1-onto→ 𝐷 )
Assertion xpf1o ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ⟨ 𝑋 , 𝑌 ⟩ ) : ( 𝐴 × 𝐶 ) –1-1-onto→ ( 𝐵 × 𝐷 ) )

Proof

Step Hyp Ref Expression
1 xpf1o.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 –1-1-onto→ 𝐵 )
2 xpf1o.2 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑌 ) : 𝐶 –1-1-onto→ 𝐷 )
3 xp1st ⊢ ( 𝑢 ∈ ( 𝐴 × 𝐶 ) → ( 1st ‘ 𝑢 ) ∈ 𝐴 )
4 3 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 × 𝐶 ) ) → ( 1st ‘ 𝑢 ) ∈ 𝐴 )
5 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑋 )
6 5 f1ompt ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 –1-1-onto→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑧 = 𝑋 ) )
7 1 6 sylib ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑧 = 𝑋 ) )
8 7 simpld ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 × 𝐶 ) ) → ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 )
10 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋
11 10 nfel1 ⊢ Ⅎ 𝑥 ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∈ 𝐵
12 csbeq1a ⊢ ( 𝑥 = ( 1st ‘ 𝑢 ) → 𝑋 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 )
13 12 eleq1d ⊢ ( 𝑥 = ( 1st ‘ 𝑢 ) → ( 𝑋 ∈ 𝐵 ↔ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) )
14 11 13 rspc ⊢ ( ( 1st ‘ 𝑢 ) ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) )
15 4 9 14 sylc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 × 𝐶 ) ) → ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∈ 𝐵 )
16 xp2nd ⊢ ( 𝑢 ∈ ( 𝐴 × 𝐶 ) → ( 2nd ‘ 𝑢 ) ∈ 𝐶 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 × 𝐶 ) ) → ( 2nd ‘ 𝑢 ) ∈ 𝐶 )
18 eqid ⊢ ( 𝑦 ∈ 𝐶 ↦ 𝑌 ) = ( 𝑦 ∈ 𝐶 ↦ 𝑌 )
19 18 f1ompt ⊢ ( ( 𝑦 ∈ 𝐶 ↦ 𝑌 ) : 𝐶 –1-1-onto→ 𝐷 ↔ ( ∀ 𝑦 ∈ 𝐶 𝑌 ∈ 𝐷 ∧ ∀ 𝑤 ∈ 𝐷 ∃! 𝑦 ∈ 𝐶 𝑤 = 𝑌 ) )
20 2 19 sylib ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐶 𝑌 ∈ 𝐷 ∧ ∀ 𝑤 ∈ 𝐷 ∃! 𝑦 ∈ 𝐶 𝑤 = 𝑌 ) )
21 20 simpld ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 𝑌 ∈ 𝐷 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 × 𝐶 ) ) → ∀ 𝑦 ∈ 𝐶 𝑌 ∈ 𝐷 )
23 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌
24 23 nfel1 ⊢ Ⅎ 𝑦 ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ∈ 𝐷
25 csbeq1a ⊢ ( 𝑦 = ( 2nd ‘ 𝑢 ) → 𝑌 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 )
26 25 eleq1d ⊢ ( 𝑦 = ( 2nd ‘ 𝑢 ) → ( 𝑌 ∈ 𝐷 ↔ ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ∈ 𝐷 ) )
27 24 26 rspc ⊢ ( ( 2nd ‘ 𝑢 ) ∈ 𝐶 → ( ∀ 𝑦 ∈ 𝐶 𝑌 ∈ 𝐷 → ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ∈ 𝐷 ) )
28 17 22 27 sylc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 × 𝐶 ) ) → ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ∈ 𝐷 )
29 15 28 opelxpd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 × 𝐶 ) ) → ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ∈ ( 𝐵 × 𝐷 ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ∈ ( 𝐵 × 𝐷 ) )
31 7 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑧 = 𝑋 )
32 31 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ∃! 𝑥 ∈ 𝐴 𝑧 = 𝑋 )
33 reu6 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝑧 = 𝑋 ↔ ∃ 𝑠 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) )
34 32 33 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑠 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) )
35 20 simprd ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐷 ∃! 𝑦 ∈ 𝐶 𝑤 = 𝑌 )
36 35 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) → ∃! 𝑦 ∈ 𝐶 𝑤 = 𝑌 )
37 reu6 ⊢ ( ∃! 𝑦 ∈ 𝐶 𝑤 = 𝑌 ↔ ∃ 𝑡 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) )
38 36 37 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) → ∃ 𝑡 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) )
39 34 38 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) ) → ( ∃ 𝑠 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ∃ 𝑡 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) )
40 reeanv ⊢ ( ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐶 ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) ↔ ( ∃ 𝑠 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ∃ 𝑡 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) )
41 pm4.38 ⊢ ( ( ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) → ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
42 41 ex ⊢ ( ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) → ( ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) → ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) ) )
43 42 ralimdv ⊢ ( ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) → ( ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) → ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) ) )
44 43 com12 ⊢ ( ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) → ( ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) → ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) ) )
45 44 ralimdv ⊢ ( ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) ) )
46 45 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
47 46 reximi ⊢ ( ∃ 𝑡 ∈ 𝐶 ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) → ∃ 𝑡 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
48 47 reximi ⊢ ( ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐶 ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) → ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
49 40 48 sylbir ⊢ ( ( ∃ 𝑠 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝑋 ↔ 𝑥 = 𝑠 ) ∧ ∃ 𝑡 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑤 = 𝑌 ↔ 𝑦 = 𝑡 ) ) → ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
50 39 49 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) ) → ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
51 vex ⊢ 𝑠 ∈ V
52 vex ⊢ 𝑡 ∈ V
53 51 52 op1std ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ( 1st ‘ 𝑢 ) = 𝑠 )
54 53 csbeq1d ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 )
55 54 eqeq2d ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ↔ 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ) )
56 51 52 op2ndd ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ( 2nd ‘ 𝑢 ) = 𝑡 )
57 56 csbeq1d ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 )
58 57 eqeq2d ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ( 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ↔ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) )
59 55 58 anbi12d ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ) )
60 eqeq1 ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ( 𝑢 = 𝑣 ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) )
61 59 60 bibi12d ⊢ ( 𝑢 = ⟨ 𝑠 , 𝑡 ⟩ → ( ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ 𝑢 = 𝑣 ) ↔ ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) ) )
62 61 ralxp ⊢ ( ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ 𝑢 = 𝑣 ) ↔ ∀ 𝑠 ∈ 𝐴 ∀ 𝑡 ∈ 𝐶 ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) )
63 nfv ⊢ Ⅎ 𝑠 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 )
64 nfcv ⊢ Ⅎ 𝑥 𝐶
65 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝑋
66 65 nfeq2 ⊢ Ⅎ 𝑥 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋
67 nfv ⊢ Ⅎ 𝑥 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌
68 66 67 nfan ⊢ Ⅎ 𝑥 ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 )
69 nfv ⊢ Ⅎ 𝑥 ⟨ 𝑠 , 𝑡 ⟩ = 𝑣
70 68 69 nfbi ⊢ Ⅎ 𝑥 ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 )
71 64 70 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑡 ∈ 𝐶 ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 )
72 nfv ⊢ Ⅎ 𝑡 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 )
73 nfv ⊢ Ⅎ 𝑦 𝑧 = 𝑋
74 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑡 / 𝑦 ⦌ 𝑌
75 74 nfeq2 ⊢ Ⅎ 𝑦 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌
76 73 75 nfan ⊢ Ⅎ 𝑦 ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 )
77 nfv ⊢ Ⅎ 𝑦 ⟨ 𝑥 , 𝑡 ⟩ = 𝑣
78 76 77 nfbi ⊢ Ⅎ 𝑦 ( ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑥 , 𝑡 ⟩ = 𝑣 )
79 csbeq1a ⊢ ( 𝑦 = 𝑡 → 𝑌 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 )
80 79 eqeq2d ⊢ ( 𝑦 = 𝑡 → ( 𝑤 = 𝑌 ↔ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) )
81 80 anbi2d ⊢ ( 𝑦 = 𝑡 → ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ) )
82 opeq2 ⊢ ( 𝑦 = 𝑡 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑡 ⟩ )
83 82 eqeq1d ⊢ ( 𝑦 = 𝑡 → ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ↔ ⟨ 𝑥 , 𝑡 ⟩ = 𝑣 ) )
84 81 83 bibi12d ⊢ ( 𝑦 = 𝑡 → ( ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ) ↔ ( ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑥 , 𝑡 ⟩ = 𝑣 ) ) )
85 72 78 84 cbvralw ⊢ ( ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ) ↔ ∀ 𝑡 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑥 , 𝑡 ⟩ = 𝑣 ) )
86 csbeq1a ⊢ ( 𝑥 = 𝑠 → 𝑋 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 )
87 86 eqeq2d ⊢ ( 𝑥 = 𝑠 → ( 𝑧 = 𝑋 ↔ 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ) )
88 87 anbi1d ⊢ ( 𝑥 = 𝑠 → ( ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ) )
89 opeq1 ⊢ ( 𝑥 = 𝑠 → ⟨ 𝑥 , 𝑡 ⟩ = ⟨ 𝑠 , 𝑡 ⟩ )
90 89 eqeq1d ⊢ ( 𝑥 = 𝑠 → ( ⟨ 𝑥 , 𝑡 ⟩ = 𝑣 ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) )
91 88 90 bibi12d ⊢ ( 𝑥 = 𝑠 → ( ( ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑥 , 𝑡 ⟩ = 𝑣 ) ↔ ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) ) )
92 91 ralbidv ⊢ ( 𝑥 = 𝑠 → ( ∀ 𝑡 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑥 , 𝑡 ⟩ = 𝑣 ) ↔ ∀ 𝑡 ∈ 𝐶 ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) ) )
93 85 92 syl5bb ⊢ ( 𝑥 = 𝑠 → ( ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ) ↔ ∀ 𝑡 ∈ 𝐶 ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) ) )
94 63 71 93 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ) ↔ ∀ 𝑠 ∈ 𝐴 ∀ 𝑡 ∈ 𝐶 ( ( 𝑧 = ⦋ 𝑠 / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ 𝑡 / 𝑦 ⦌ 𝑌 ) ↔ ⟨ 𝑠 , 𝑡 ⟩ = 𝑣 ) )
95 62 94 bitr4i ⊢ ( ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ 𝑢 = 𝑣 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ) )
96 eqeq2 ⊢ ( 𝑣 = ⟨ 𝑠 , 𝑡 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑠 , 𝑡 ⟩ ) )
97 vex ⊢ 𝑥 ∈ V
98 vex ⊢ 𝑦 ∈ V
99 97 98 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑠 , 𝑡 ⟩ ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) )
100 96 99 bitrdi ⊢ ( 𝑣 = ⟨ 𝑠 , 𝑡 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
101 100 bibi2d ⊢ ( 𝑣 = ⟨ 𝑠 , 𝑡 ⟩ → ( ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ) ↔ ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) ) )
102 101 2ralbidv ⊢ ( 𝑣 = ⟨ 𝑠 , 𝑡 ⟩ → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝑣 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) ) )
103 95 102 syl5bb ⊢ ( 𝑣 = ⟨ 𝑠 , 𝑡 ⟩ → ( ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ 𝑢 = 𝑣 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) ) )
104 103 rexxp ⊢ ( ∃ 𝑣 ∈ ( 𝐴 × 𝐶 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ 𝑢 = 𝑣 ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑌 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) ) )
105 50 104 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) ) → ∃ 𝑣 ∈ ( 𝐴 × 𝐶 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ 𝑢 = 𝑣 ) )
106 reu6 ⊢ ( ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ ∃ 𝑣 ∈ ( 𝐴 × 𝐶 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ( ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ↔ 𝑢 = 𝑣 ) )
107 105 106 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) ) → ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) )
108 107 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐷 ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) )
109 eqeq1 ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑣 = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ↔ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ) )
110 vex ⊢ 𝑧 ∈ V
111 vex ⊢ 𝑤 ∈ V
112 110 111 opth ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ↔ ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) )
113 109 112 bitrdi ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑣 = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ↔ ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ) )
114 113 reubidv ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) 𝑣 = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ↔ ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) ) )
115 114 ralxp ⊢ ( ∀ 𝑣 ∈ ( 𝐵 × 𝐷 ) ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) 𝑣 = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐷 ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) ( 𝑧 = ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 ∧ 𝑤 = ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ) )
116 108 115 sylibr ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( 𝐵 × 𝐷 ) ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) 𝑣 = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ )
117 nfcv ⊢ Ⅎ 𝑧 ⟨ 𝑋 , 𝑌 ⟩
118 nfcv ⊢ Ⅎ 𝑤 ⟨ 𝑋 , 𝑌 ⟩
119 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑋
120 nfcv ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑦 ⦌ 𝑌
121 119 120 nfop ⊢ Ⅎ 𝑥 ⟨ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 , ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ⟩
122 nfcv ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝑋
123 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝑌
124 122 123 nfop ⊢ Ⅎ 𝑦 ⟨ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 , ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ⟩
125 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝑋 = ⦋ 𝑧 / 𝑥 ⦌ 𝑋 )
126 csbeq1a ⊢ ( 𝑦 = 𝑤 → 𝑌 = ⦋ 𝑤 / 𝑦 ⦌ 𝑌 )
127 opeq12 ⊢ ( ( 𝑋 = ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∧ 𝑌 = ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ) → ⟨ 𝑋 , 𝑌 ⟩ = ⟨ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 , ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ⟩ )
128 125 126 127 syl2an ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ⟨ 𝑋 , 𝑌 ⟩ = ⟨ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 , ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ⟩ )
129 117 118 121 124 128 cbvmpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐶 ↦ ⟨ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 , ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ⟩ )
130 110 111 op1std ⊢ ( 𝑢 = ⟨ 𝑧 , 𝑤 ⟩ → ( 1st ‘ 𝑢 ) = 𝑧 )
131 130 csbeq1d ⊢ ( 𝑢 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 = ⦋ 𝑧 / 𝑥 ⦌ 𝑋 )
132 110 111 op2ndd ⊢ ( 𝑢 = ⟨ 𝑧 , 𝑤 ⟩ → ( 2nd ‘ 𝑢 ) = 𝑤 )
133 132 csbeq1d ⊢ ( 𝑢 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 = ⦋ 𝑤 / 𝑦 ⦌ 𝑌 )
134 131 133 opeq12d ⊢ ( 𝑢 = ⟨ 𝑧 , 𝑤 ⟩ → ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ = ⟨ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 , ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ⟩ )
135 134 mpompt ⊢ ( 𝑢 ∈ ( 𝐴 × 𝐶 ) ↦ ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐶 ↦ ⟨ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 , ⦋ 𝑤 / 𝑦 ⦌ 𝑌 ⟩ )
136 129 135 eqtr4i ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑢 ∈ ( 𝐴 × 𝐶 ) ↦ ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ )
137 136 f1ompt ⊢ ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ⟨ 𝑋 , 𝑌 ⟩ ) : ( 𝐴 × 𝐶 ) –1-1-onto→ ( 𝐵 × 𝐷 ) ↔ ( ∀ 𝑢 ∈ ( 𝐴 × 𝐶 ) ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ∈ ( 𝐵 × 𝐷 ) ∧ ∀ 𝑣 ∈ ( 𝐵 × 𝐷 ) ∃! 𝑢 ∈ ( 𝐴 × 𝐶 ) 𝑣 = ⟨ ⦋ ( 1st ‘ 𝑢 ) / 𝑥 ⦌ 𝑋 , ⦋ ( 2nd ‘ 𝑢 ) / 𝑦 ⦌ 𝑌 ⟩ ) )
138 30 116 137 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ⟨ 𝑋 , 𝑌 ⟩ ) : ( 𝐴 × 𝐶 ) –1-1-onto→ ( 𝐵 × 𝐷 ) )