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

Theorem xpf1o 8163
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 7242 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (1st𝑢) ∈ 𝐴)
21adantl 481 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) ∈ 𝐴)
3 xpf1o.1 . . . . . . . 8 (𝜑 → (𝑥𝐴𝑋):𝐴1-1-onto𝐵)
4 eqid 2651 . . . . . . . . 9 (𝑥𝐴𝑋) = (𝑥𝐴𝑋)
54f1ompt 6422 . . . . . . . 8 ((𝑥𝐴𝑋):𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
63, 5sylib 208 . . . . . . 7 (𝜑 → (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
76simpld 474 . . . . . 6 (𝜑 → ∀𝑥𝐴 𝑋𝐵)
87adantr 480 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑥𝐴 𝑋𝐵)
9 nfcsb1v 3582 . . . . . . 7 𝑥(1st𝑢) / 𝑥𝑋
109nfel1 2808 . . . . . 6 𝑥(1st𝑢) / 𝑥𝑋𝐵
11 csbeq1a 3575 . . . . . . 7 (𝑥 = (1st𝑢) → 𝑋 = (1st𝑢) / 𝑥𝑋)
1211eleq1d 2715 . . . . . 6 (𝑥 = (1st𝑢) → (𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
1310, 12rspc 3334 . . . . 5 ((1st𝑢) ∈ 𝐴 → (∀𝑥𝐴 𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
142, 8, 13sylc 65 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) / 𝑥𝑋𝐵)
15 xp2nd 7243 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (2nd𝑢) ∈ 𝐶)
1615adantl 481 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) ∈ 𝐶)
17 xpf1o.2 . . . . . . . 8 (𝜑 → (𝑦𝐶𝑌):𝐶1-1-onto𝐷)
18 eqid 2651 . . . . . . . . 9 (𝑦𝐶𝑌) = (𝑦𝐶𝑌)
1918f1ompt 6422 . . . . . . . 8 ((𝑦𝐶𝑌):𝐶1-1-onto𝐷 ↔ (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2017, 19sylib 208 . . . . . . 7 (𝜑 → (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2120simpld 474 . . . . . 6 (𝜑 → ∀𝑦𝐶 𝑌𝐷)
2221adantr 480 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑦𝐶 𝑌𝐷)
23 nfcsb1v 3582 . . . . . . 7 𝑦(2nd𝑢) / 𝑦𝑌
2423nfel1 2808 . . . . . 6 𝑦(2nd𝑢) / 𝑦𝑌𝐷
25 csbeq1a 3575 . . . . . . 7 (𝑦 = (2nd𝑢) → 𝑌 = (2nd𝑢) / 𝑦𝑌)
2625eleq1d 2715 . . . . . 6 (𝑦 = (2nd𝑢) → (𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2724, 26rspc 3334 . . . . 5 ((2nd𝑢) ∈ 𝐶 → (∀𝑦𝐶 𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2816, 22, 27sylc 65 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) / 𝑦𝑌𝐷)
29 opelxpi 5182 . . . 4 (((1st𝑢) / 𝑥𝑋𝐵(2nd𝑢) / 𝑦𝑌𝐷) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3014, 28, 29syl2anc 694 . . 3 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3130ralrimiva 2995 . 2 (𝜑 → ∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
326simprd 478 . . . . . . . . . 10 (𝜑 → ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋)
3332r19.21bi 2961 . . . . . . . . 9 ((𝜑𝑧𝐵) → ∃!𝑥𝐴 𝑧 = 𝑋)
34 reu6 3428 . . . . . . . . 9 (∃!𝑥𝐴 𝑧 = 𝑋 ↔ ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3533, 34sylib 208 . . . . . . . 8 ((𝜑𝑧𝐵) → ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3620simprd 478 . . . . . . . . . 10 (𝜑 → ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌)
3736r19.21bi 2961 . . . . . . . . 9 ((𝜑𝑤𝐷) → ∃!𝑦𝐶 𝑤 = 𝑌)
38 reu6 3428 . . . . . . . . 9 (∃!𝑦𝐶 𝑤 = 𝑌 ↔ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
3937, 38sylib 208 . . . . . . . 8 ((𝜑𝑤𝐷) → ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
4035, 39anim12dan 900 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
41 reeanv 3136 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) ↔ (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
42 pm4.38 934 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑋𝑥 = 𝑠) ∧ (𝑤 = 𝑌𝑦 = 𝑡)) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4342ex 449 . . . . . . . . . . . . . 14 ((𝑧 = 𝑋𝑥 = 𝑠) → ((𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4443ralimdv 2992 . . . . . . . . . . . . 13 ((𝑧 = 𝑋𝑥 = 𝑠) → (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4544com12 32 . . . . . . . . . . . 12 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4645ralimdv 2992 . . . . . . . . . . 11 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4746impcom 445 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4847reximi 3040 . . . . . . . . 9 (∃𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4948reximi 3040 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5041, 49sylbir 225 . . . . . . 7 ((∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5140, 50syl 17 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
52 vex 3234 . . . . . . . . . . . . . . 15 𝑠 ∈ V
53 vex 3234 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5452, 53op1std 7220 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) = 𝑠)
5554csbeq1d 3573 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) / 𝑥𝑋 = 𝑠 / 𝑥𝑋)
5655eqeq2d 2661 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑧 = (1st𝑢) / 𝑥𝑋𝑧 = 𝑠 / 𝑥𝑋))
5752, 53op2ndd 7221 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) = 𝑡)
5857csbeq1d 3573 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑡 / 𝑦𝑌)
5958eqeq2d 2661 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑤 = (2nd𝑢) / 𝑦𝑌𝑤 = 𝑡 / 𝑦𝑌))
6056, 59anbi12d 747 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → ((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
61 eqeq1 2655 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑢 = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
6260, 61bibi12d 334 . . . . . . . . . 10 (𝑢 = ⟨𝑠, 𝑡⟩ → (((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
6362ralxp 5296 . . . . . . . . 9 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
64 nfv 1883 . . . . . . . . . 10 𝑠𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
65 nfcv 2793 . . . . . . . . . . 11 𝑥𝐶
66 nfcsb1v 3582 . . . . . . . . . . . . . 14 𝑥𝑠 / 𝑥𝑋
6766nfeq2 2809 . . . . . . . . . . . . 13 𝑥 𝑧 = 𝑠 / 𝑥𝑋
68 nfv 1883 . . . . . . . . . . . . 13 𝑥 𝑤 = 𝑡 / 𝑦𝑌
6967, 68nfan 1868 . . . . . . . . . . . 12 𝑥(𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)
70 nfv 1883 . . . . . . . . . . . 12 𝑥𝑠, 𝑡⟩ = 𝑣
7169, 70nfbi 1873 . . . . . . . . . . 11 𝑥((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
7265, 71nfral 2974 . . . . . . . . . 10 𝑥𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
73 nfv 1883 . . . . . . . . . . . 12 𝑡((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
74 nfv 1883 . . . . . . . . . . . . . 14 𝑦 𝑧 = 𝑋
75 nfcsb1v 3582 . . . . . . . . . . . . . . 15 𝑦𝑡 / 𝑦𝑌
7675nfeq2 2809 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑡 / 𝑦𝑌
7774, 76nfan 1868 . . . . . . . . . . . . 13 𝑦(𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)
78 nfv 1883 . . . . . . . . . . . . 13 𝑦𝑥, 𝑡⟩ = 𝑣
7977, 78nfbi 1873 . . . . . . . . . . . 12 𝑦((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)
80 csbeq1a 3575 . . . . . . . . . . . . . . 15 (𝑦 = 𝑡𝑌 = 𝑡 / 𝑦𝑌)
8180eqeq2d 2661 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → (𝑤 = 𝑌𝑤 = 𝑡 / 𝑦𝑌))
8281anbi2d 740 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)))
83 opeq2 4434 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑡⟩)
8483eqeq1d 2653 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
8582, 84bibi12d 334 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)))
8673, 79, 85cbvral 3197 . . . . . . . . . . 11 (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
87 csbeq1a 3575 . . . . . . . . . . . . . . 15 (𝑥 = 𝑠𝑋 = 𝑠 / 𝑥𝑋)
8887eqeq2d 2661 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → (𝑧 = 𝑋𝑧 = 𝑠 / 𝑥𝑋))
8988anbi1d 741 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
90 opeq1 4433 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → ⟨𝑥, 𝑡⟩ = ⟨𝑠, 𝑡⟩)
9190eqeq1d 2653 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (⟨𝑥, 𝑡⟩ = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9289, 91bibi12d 334 . . . . . . . . . . . 12 (𝑥 = 𝑠 → (((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9392ralbidv 3015 . . . . . . . . . . 11 (𝑥 = 𝑠 → (∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9486, 93syl5bb 272 . . . . . . . . . 10 (𝑥 = 𝑠 → (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9564, 72, 94cbvral 3197 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9663, 95bitr4i 267 . . . . . . . 8 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣))
97 eqeq2 2662 . . . . . . . . . . 11 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩))
98 vex 3234 . . . . . . . . . . . 12 𝑥 ∈ V
99 vex 3234 . . . . . . . . . . . 12 𝑦 ∈ V
10098, 99opth 4974 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩ ↔ (𝑥 = 𝑠𝑦 = 𝑡))
10197, 100syl6bb 276 . . . . . . . . . 10 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
102101bibi2d 331 . . . . . . . . 9 (𝑣 = ⟨𝑠, 𝑡⟩ → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
1031022ralbidv 3018 . . . . . . . 8 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
10496, 103syl5bb 272 . . . . . . 7 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
105104rexxp 5297 . . . . . 6 (∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
10651, 105sylibr 224 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
107 reu6 3428 . . . . 5 (∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
108106, 107sylibr 224 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
109108ralrimivva 3000 . . 3 (𝜑 → ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
110 eqeq1 2655 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
111 vex 3234 . . . . . . 7 𝑧 ∈ V
112 vex 3234 . . . . . . 7 𝑤 ∈ V
113111, 112opth 4974 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
114110, 113syl6bb 276 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
115114reubidv 3156 . . . 4 (𝑣 = ⟨𝑧, 𝑤⟩ → (∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
116115ralxp 5296 . . 3 (∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
117109, 116sylibr 224 . 2 (𝜑 → ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
118 nfcv 2793 . . . . 5 𝑧𝑋, 𝑌
119 nfcv 2793 . . . . 5 𝑤𝑋, 𝑌
120 nfcsb1v 3582 . . . . . 6 𝑥𝑧 / 𝑥𝑋
121 nfcv 2793 . . . . . 6 𝑥𝑤 / 𝑦𝑌
122120, 121nfop 4449 . . . . 5 𝑥𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
123 nfcv 2793 . . . . . 6 𝑦𝑧 / 𝑥𝑋
124 nfcsb1v 3582 . . . . . 6 𝑦𝑤 / 𝑦𝑌
125123, 124nfop 4449 . . . . 5 𝑦𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
126 csbeq1a 3575 . . . . . 6 (𝑥 = 𝑧𝑋 = 𝑧 / 𝑥𝑋)
127 csbeq1a 3575 . . . . . 6 (𝑦 = 𝑤𝑌 = 𝑤 / 𝑦𝑌)
128 opeq12 4435 . . . . . 6 ((𝑋 = 𝑧 / 𝑥𝑋𝑌 = 𝑤 / 𝑦𝑌) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
129126, 127, 128syl2an 493 . . . . 5 ((𝑥 = 𝑧𝑦 = 𝑤) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
130118, 119, 122, 125, 129cbvmpt2 6776 . . . 4 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
131111, 112op1std 7220 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) = 𝑧)
132131csbeq1d 3573 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) / 𝑥𝑋 = 𝑧 / 𝑥𝑋)
133111, 112op2ndd 7221 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) = 𝑤)
134133csbeq1d 3573 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑤 / 𝑦𝑌)
135132, 134opeq12d 4441 . . . . 5 (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
136135mpt2mpt 6794 . . . 4 (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
137130, 136eqtr4i 2676 . . 3 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
138137f1ompt 6422 . 2 ((𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷) ↔ (∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷) ∧ ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
13931, 117, 138sylanbrc 699 1 (𝜑 → (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  wrex 2942  ∃!wreu 2943  csb 3566  cop 4216  cmpt 4762   × cxp 5141  1-1-ontowf1o 5925  cfv 5926  cmpt2 6692  1st c1st 7208  2nd c2nd 7209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211
This theorem is referenced by:  infxpenc  8879  pwfseqlem5  9523
  Copyright terms: Public domain W3C validator