Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpf1o Structured version   Visualization version   GIF version

Theorem xpf1o 8007
 Description: Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015.)
Hypotheses
Ref Expression
xpf1o.1 (𝜑 → (𝑥𝐴𝑋):𝐴1-1-onto𝐵)
xpf1o.2 (𝜑 → (𝑦𝐶𝑌):𝐶1-1-onto𝐷)
Assertion
Ref Expression
xpf1o (𝜑 → (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐶,𝑦   𝑦,𝑋   𝑥,𝐵   𝑦,𝐷   𝑥,𝑌
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑦)   𝐷(𝑥)   𝑋(𝑥)   𝑌(𝑦)

Proof of Theorem xpf1o
Dummy variables 𝑡 𝑠 𝑢 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xp1st 7089 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (1st𝑢) ∈ 𝐴)
21adantl 481 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) ∈ 𝐴)
3 xpf1o.1 . . . . . . . 8 (𝜑 → (𝑥𝐴𝑋):𝐴1-1-onto𝐵)
4 eqid 2610 . . . . . . . . 9 (𝑥𝐴𝑋) = (𝑥𝐴𝑋)
54f1ompt 6290 . . . . . . . 8 ((𝑥𝐴𝑋):𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
63, 5sylib 207 . . . . . . 7 (𝜑 → (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
76simpld 474 . . . . . 6 (𝜑 → ∀𝑥𝐴 𝑋𝐵)
87adantr 480 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑥𝐴 𝑋𝐵)
9 nfcsb1v 3515 . . . . . . 7 𝑥(1st𝑢) / 𝑥𝑋
109nfel1 2765 . . . . . 6 𝑥(1st𝑢) / 𝑥𝑋𝐵
11 csbeq1a 3508 . . . . . . 7 (𝑥 = (1st𝑢) → 𝑋 = (1st𝑢) / 𝑥𝑋)
1211eleq1d 2672 . . . . . 6 (𝑥 = (1st𝑢) → (𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
1310, 12rspc 3276 . . . . 5 ((1st𝑢) ∈ 𝐴 → (∀𝑥𝐴 𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
142, 8, 13sylc 63 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) / 𝑥𝑋𝐵)
15 xp2nd 7090 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (2nd𝑢) ∈ 𝐶)
1615adantl 481 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) ∈ 𝐶)
17 xpf1o.2 . . . . . . . 8 (𝜑 → (𝑦𝐶𝑌):𝐶1-1-onto𝐷)
18 eqid 2610 . . . . . . . . 9 (𝑦𝐶𝑌) = (𝑦𝐶𝑌)
1918f1ompt 6290 . . . . . . . 8 ((𝑦𝐶𝑌):𝐶1-1-onto𝐷 ↔ (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2017, 19sylib 207 . . . . . . 7 (𝜑 → (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2120simpld 474 . . . . . 6 (𝜑 → ∀𝑦𝐶 𝑌𝐷)
2221adantr 480 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑦𝐶 𝑌𝐷)
23 nfcsb1v 3515 . . . . . . 7 𝑦(2nd𝑢) / 𝑦𝑌
2423nfel1 2765 . . . . . 6 𝑦(2nd𝑢) / 𝑦𝑌𝐷
25 csbeq1a 3508 . . . . . . 7 (𝑦 = (2nd𝑢) → 𝑌 = (2nd𝑢) / 𝑦𝑌)
2625eleq1d 2672 . . . . . 6 (𝑦 = (2nd𝑢) → (𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2724, 26rspc 3276 . . . . 5 ((2nd𝑢) ∈ 𝐶 → (∀𝑦𝐶 𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2816, 22, 27sylc 63 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) / 𝑦𝑌𝐷)
29 opelxpi 5072 . . . 4 (((1st𝑢) / 𝑥𝑋𝐵(2nd𝑢) / 𝑦𝑌𝐷) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3014, 28, 29syl2anc 691 . . 3 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3130ralrimiva 2949 . 2 (𝜑 → ∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
326simprd 478 . . . . . . . . . 10 (𝜑 → ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋)
3332r19.21bi 2916 . . . . . . . . 9 ((𝜑𝑧𝐵) → ∃!𝑥𝐴 𝑧 = 𝑋)
34 reu6 3362 . . . . . . . . 9 (∃!𝑥𝐴 𝑧 = 𝑋 ↔ ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3533, 34sylib 207 . . . . . . . 8 ((𝜑𝑧𝐵) → ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3620simprd 478 . . . . . . . . . 10 (𝜑 → ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌)
3736r19.21bi 2916 . . . . . . . . 9 ((𝜑𝑤𝐷) → ∃!𝑦𝐶 𝑤 = 𝑌)
38 reu6 3362 . . . . . . . . 9 (∃!𝑦𝐶 𝑤 = 𝑌 ↔ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
3937, 38sylib 207 . . . . . . . 8 ((𝜑𝑤𝐷) → ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
4035, 39anim12dan 878 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
41 reeanv 3086 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) ↔ (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
42 pm4.38 912 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑋𝑥 = 𝑠) ∧ (𝑤 = 𝑌𝑦 = 𝑡)) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4342ex 449 . . . . . . . . . . . . . 14 ((𝑧 = 𝑋𝑥 = 𝑠) → ((𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4443ralimdv 2946 . . . . . . . . . . . . 13 ((𝑧 = 𝑋𝑥 = 𝑠) → (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4544com12 32 . . . . . . . . . . . 12 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4645ralimdv 2946 . . . . . . . . . . 11 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4746impcom 445 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4847reximi 2994 . . . . . . . . 9 (∃𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4948reximi 2994 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5041, 49sylbir 224 . . . . . . 7 ((∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5140, 50syl 17 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
52 vex 3176 . . . . . . . . . . . . . . 15 𝑠 ∈ V
53 vex 3176 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5452, 53op1std 7069 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) = 𝑠)
5554csbeq1d 3506 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) / 𝑥𝑋 = 𝑠 / 𝑥𝑋)
5655eqeq2d 2620 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑧 = (1st𝑢) / 𝑥𝑋𝑧 = 𝑠 / 𝑥𝑋))
5752, 53op2ndd 7070 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) = 𝑡)
5857csbeq1d 3506 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑡 / 𝑦𝑌)
5958eqeq2d 2620 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑤 = (2nd𝑢) / 𝑦𝑌𝑤 = 𝑡 / 𝑦𝑌))
6056, 59anbi12d 743 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → ((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
61 eqeq1 2614 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑢 = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
6260, 61bibi12d 334 . . . . . . . . . 10 (𝑢 = ⟨𝑠, 𝑡⟩ → (((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
6362ralxp 5185 . . . . . . . . 9 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
64 nfv 1830 . . . . . . . . . 10 𝑠𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
65 nfcv 2751 . . . . . . . . . . 11 𝑥𝐶
66 nfcsb1v 3515 . . . . . . . . . . . . . 14 𝑥𝑠 / 𝑥𝑋
6766nfeq2 2766 . . . . . . . . . . . . 13 𝑥 𝑧 = 𝑠 / 𝑥𝑋
68 nfv 1830 . . . . . . . . . . . . 13 𝑥 𝑤 = 𝑡 / 𝑦𝑌
6967, 68nfan 1816 . . . . . . . . . . . 12 𝑥(𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)
70 nfv 1830 . . . . . . . . . . . 12 𝑥𝑠, 𝑡⟩ = 𝑣
7169, 70nfbi 1821 . . . . . . . . . . 11 𝑥((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
7265, 71nfral 2929 . . . . . . . . . 10 𝑥𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
73 nfv 1830 . . . . . . . . . . . 12 𝑡((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
74 nfv 1830 . . . . . . . . . . . . . 14 𝑦 𝑧 = 𝑋
75 nfcsb1v 3515 . . . . . . . . . . . . . . 15 𝑦𝑡 / 𝑦𝑌
7675nfeq2 2766 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑡 / 𝑦𝑌
7774, 76nfan 1816 . . . . . . . . . . . . 13 𝑦(𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)
78 nfv 1830 . . . . . . . . . . . . 13 𝑦𝑥, 𝑡⟩ = 𝑣
7977, 78nfbi 1821 . . . . . . . . . . . 12 𝑦((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)
80 csbeq1a 3508 . . . . . . . . . . . . . . 15 (𝑦 = 𝑡𝑌 = 𝑡 / 𝑦𝑌)
8180eqeq2d 2620 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → (𝑤 = 𝑌𝑤 = 𝑡 / 𝑦𝑌))
8281anbi2d 736 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)))
83 opeq2 4341 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑡⟩)
8483eqeq1d 2612 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
8582, 84bibi12d 334 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)))
8673, 79, 85cbvral 3143 . . . . . . . . . . 11 (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
87 csbeq1a 3508 . . . . . . . . . . . . . . 15 (𝑥 = 𝑠𝑋 = 𝑠 / 𝑥𝑋)
8887eqeq2d 2620 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → (𝑧 = 𝑋𝑧 = 𝑠 / 𝑥𝑋))
8988anbi1d 737 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
90 opeq1 4340 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → ⟨𝑥, 𝑡⟩ = ⟨𝑠, 𝑡⟩)
9190eqeq1d 2612 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (⟨𝑥, 𝑡⟩ = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9289, 91bibi12d 334 . . . . . . . . . . . 12 (𝑥 = 𝑠 → (((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9392ralbidv 2969 . . . . . . . . . . 11 (𝑥 = 𝑠 → (∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9486, 93syl5bb 271 . . . . . . . . . 10 (𝑥 = 𝑠 → (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9564, 72, 94cbvral 3143 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9663, 95bitr4i 266 . . . . . . . 8 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣))
97 eqeq2 2621 . . . . . . . . . . 11 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩))
98 vex 3176 . . . . . . . . . . . 12 𝑥 ∈ V
99 vex 3176 . . . . . . . . . . . 12 𝑦 ∈ V
10098, 99opth 4871 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩ ↔ (𝑥 = 𝑠𝑦 = 𝑡))
10197, 100syl6bb 275 . . . . . . . . . 10 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
102101bibi2d 331 . . . . . . . . 9 (𝑣 = ⟨𝑠, 𝑡⟩ → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
1031022ralbidv 2972 . . . . . . . 8 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
10496, 103syl5bb 271 . . . . . . 7 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
105104rexxp 5186 . . . . . 6 (∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
10651, 105sylibr 223 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
107 reu6 3362 . . . . 5 (∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
108106, 107sylibr 223 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
109108ralrimivva 2954 . . 3 (𝜑 → ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
110 eqeq1 2614 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
111 vex 3176 . . . . . . 7 𝑧 ∈ V
112 vex 3176 . . . . . . 7 𝑤 ∈ V
113111, 112opth 4871 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
114110, 113syl6bb 275 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
115114reubidv 3103 . . . 4 (𝑣 = ⟨𝑧, 𝑤⟩ → (∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
116115ralxp 5185 . . 3 (∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
117109, 116sylibr 223 . 2 (𝜑 → ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
118 nfcv 2751 . . . . 5 𝑧𝑋, 𝑌
119 nfcv 2751 . . . . 5 𝑤𝑋, 𝑌
120 nfcsb1v 3515 . . . . . 6 𝑥𝑧 / 𝑥𝑋
121 nfcv 2751 . . . . . 6 𝑥𝑤 / 𝑦𝑌
122120, 121nfop 4356 . . . . 5 𝑥𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
123 nfcv 2751 . . . . . 6 𝑦𝑧 / 𝑥𝑋
124 nfcsb1v 3515 . . . . . 6 𝑦𝑤 / 𝑦𝑌
125123, 124nfop 4356 . . . . 5 𝑦𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
126 csbeq1a 3508 . . . . . 6 (𝑥 = 𝑧𝑋 = 𝑧 / 𝑥𝑋)
127 csbeq1a 3508 . . . . . 6 (𝑦 = 𝑤𝑌 = 𝑤 / 𝑦𝑌)
128 opeq12 4342 . . . . . 6 ((𝑋 = 𝑧 / 𝑥𝑋𝑌 = 𝑤 / 𝑦𝑌) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
129126, 127, 128syl2an 493 . . . . 5 ((𝑥 = 𝑧𝑦 = 𝑤) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
130118, 119, 122, 125, 129cbvmpt2 6632 . . . 4 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
131111, 112op1std 7069 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) = 𝑧)
132131csbeq1d 3506 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) / 𝑥𝑋 = 𝑧 / 𝑥𝑋)
133111, 112op2ndd 7070 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) = 𝑤)
134133csbeq1d 3506 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑤 / 𝑦𝑌)
135132, 134opeq12d 4348 . . . . 5 (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
136135mpt2mpt 6650 . . . 4 (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
137130, 136eqtr4i 2635 . . 3 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
138137f1ompt 6290 . 2 ((𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷) ↔ (∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷) ∧ ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
13931, 117, 138sylanbrc 695 1 (𝜑 → (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ⦋csb 3499  ⟨cop 4131   ↦ cmpt 4643   × cxp 5036  –1-1-onto→wf1o 5803  ‘cfv 5804   ↦ cmpt2 6551  1st c1st 7057  2nd c2nd 7058 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060 This theorem is referenced by:  infxpenc  8724  pwfseqlem5  9364
 Copyright terms: Public domain W3C validator