ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpf1o GIF version

Theorem xpf1o 6838
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 6160 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (1st𝑢) ∈ 𝐴)
21adantl 277 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) ∈ 𝐴)
3 xpf1o.1 . . . . . . . 8 (𝜑 → (𝑥𝐴𝑋):𝐴1-1-onto𝐵)
4 eqid 2177 . . . . . . . . 9 (𝑥𝐴𝑋) = (𝑥𝐴𝑋)
54f1ompt 5663 . . . . . . . 8 ((𝑥𝐴𝑋):𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
63, 5sylib 122 . . . . . . 7 (𝜑 → (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
76simpld 112 . . . . . 6 (𝜑 → ∀𝑥𝐴 𝑋𝐵)
87adantr 276 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑥𝐴 𝑋𝐵)
9 nfcsb1v 3090 . . . . . . 7 𝑥(1st𝑢) / 𝑥𝑋
109nfel1 2330 . . . . . 6 𝑥(1st𝑢) / 𝑥𝑋𝐵
11 csbeq1a 3066 . . . . . . 7 (𝑥 = (1st𝑢) → 𝑋 = (1st𝑢) / 𝑥𝑋)
1211eleq1d 2246 . . . . . 6 (𝑥 = (1st𝑢) → (𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
1310, 12rspc 2835 . . . . 5 ((1st𝑢) ∈ 𝐴 → (∀𝑥𝐴 𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
142, 8, 13sylc 62 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) / 𝑥𝑋𝐵)
15 xp2nd 6161 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (2nd𝑢) ∈ 𝐶)
1615adantl 277 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) ∈ 𝐶)
17 xpf1o.2 . . . . . . . 8 (𝜑 → (𝑦𝐶𝑌):𝐶1-1-onto𝐷)
18 eqid 2177 . . . . . . . . 9 (𝑦𝐶𝑌) = (𝑦𝐶𝑌)
1918f1ompt 5663 . . . . . . . 8 ((𝑦𝐶𝑌):𝐶1-1-onto𝐷 ↔ (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2017, 19sylib 122 . . . . . . 7 (𝜑 → (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2120simpld 112 . . . . . 6 (𝜑 → ∀𝑦𝐶 𝑌𝐷)
2221adantr 276 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑦𝐶 𝑌𝐷)
23 nfcsb1v 3090 . . . . . . 7 𝑦(2nd𝑢) / 𝑦𝑌
2423nfel1 2330 . . . . . 6 𝑦(2nd𝑢) / 𝑦𝑌𝐷
25 csbeq1a 3066 . . . . . . 7 (𝑦 = (2nd𝑢) → 𝑌 = (2nd𝑢) / 𝑦𝑌)
2625eleq1d 2246 . . . . . 6 (𝑦 = (2nd𝑢) → (𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2724, 26rspc 2835 . . . . 5 ((2nd𝑢) ∈ 𝐶 → (∀𝑦𝐶 𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2816, 22, 27sylc 62 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) / 𝑦𝑌𝐷)
29 opelxpi 4655 . . . 4 (((1st𝑢) / 𝑥𝑋𝐵(2nd𝑢) / 𝑦𝑌𝐷) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3014, 28, 29syl2anc 411 . . 3 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3130ralrimiva 2550 . 2 (𝜑 → ∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
326simprd 114 . . . . . . . . . 10 (𝜑 → ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋)
3332r19.21bi 2565 . . . . . . . . 9 ((𝜑𝑧𝐵) → ∃!𝑥𝐴 𝑧 = 𝑋)
34 reu6 2926 . . . . . . . . 9 (∃!𝑥𝐴 𝑧 = 𝑋 ↔ ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3533, 34sylib 122 . . . . . . . 8 ((𝜑𝑧𝐵) → ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3620simprd 114 . . . . . . . . . 10 (𝜑 → ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌)
3736r19.21bi 2565 . . . . . . . . 9 ((𝜑𝑤𝐷) → ∃!𝑦𝐶 𝑤 = 𝑌)
38 reu6 2926 . . . . . . . . 9 (∃!𝑦𝐶 𝑤 = 𝑌 ↔ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
3937, 38sylib 122 . . . . . . . 8 ((𝜑𝑤𝐷) → ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
4035, 39anim12dan 600 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
41 reeanv 2646 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) ↔ (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
42 pm4.38 605 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑋𝑥 = 𝑠) ∧ (𝑤 = 𝑌𝑦 = 𝑡)) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4342ex 115 . . . . . . . . . . . . . 14 ((𝑧 = 𝑋𝑥 = 𝑠) → ((𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4443ralimdv 2545 . . . . . . . . . . . . 13 ((𝑧 = 𝑋𝑥 = 𝑠) → (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4544com12 30 . . . . . . . . . . . 12 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4645ralimdv 2545 . . . . . . . . . . 11 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4746impcom 125 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4847reximi 2574 . . . . . . . . 9 (∃𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4948reximi 2574 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5041, 49sylbir 135 . . . . . . 7 ((∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5140, 50syl 14 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
52 vex 2740 . . . . . . . . . . . . . . 15 𝑠 ∈ V
53 vex 2740 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5452, 53op1std 6143 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) = 𝑠)
5554csbeq1d 3064 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) / 𝑥𝑋 = 𝑠 / 𝑥𝑋)
5655eqeq2d 2189 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑧 = (1st𝑢) / 𝑥𝑋𝑧 = 𝑠 / 𝑥𝑋))
5752, 53op2ndd 6144 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) = 𝑡)
5857csbeq1d 3064 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑡 / 𝑦𝑌)
5958eqeq2d 2189 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑤 = (2nd𝑢) / 𝑦𝑌𝑤 = 𝑡 / 𝑦𝑌))
6056, 59anbi12d 473 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → ((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
61 eqeq1 2184 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑢 = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
6260, 61bibi12d 235 . . . . . . . . . 10 (𝑢 = ⟨𝑠, 𝑡⟩ → (((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
6362ralxp 4766 . . . . . . . . 9 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
64 nfv 1528 . . . . . . . . . 10 𝑠𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
65 nfcv 2319 . . . . . . . . . . 11 𝑥𝐶
66 nfcsb1v 3090 . . . . . . . . . . . . . 14 𝑥𝑠 / 𝑥𝑋
6766nfeq2 2331 . . . . . . . . . . . . 13 𝑥 𝑧 = 𝑠 / 𝑥𝑋
68 nfv 1528 . . . . . . . . . . . . 13 𝑥 𝑤 = 𝑡 / 𝑦𝑌
6967, 68nfan 1565 . . . . . . . . . . . 12 𝑥(𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)
70 nfv 1528 . . . . . . . . . . . 12 𝑥𝑠, 𝑡⟩ = 𝑣
7169, 70nfbi 1589 . . . . . . . . . . 11 𝑥((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
7265, 71nfralxy 2515 . . . . . . . . . 10 𝑥𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
73 nfv 1528 . . . . . . . . . . . 12 𝑡((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
74 nfv 1528 . . . . . . . . . . . . . 14 𝑦 𝑧 = 𝑋
75 nfcsb1v 3090 . . . . . . . . . . . . . . 15 𝑦𝑡 / 𝑦𝑌
7675nfeq2 2331 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑡 / 𝑦𝑌
7774, 76nfan 1565 . . . . . . . . . . . . 13 𝑦(𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)
78 nfv 1528 . . . . . . . . . . . . 13 𝑦𝑥, 𝑡⟩ = 𝑣
7977, 78nfbi 1589 . . . . . . . . . . . 12 𝑦((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)
80 csbeq1a 3066 . . . . . . . . . . . . . . 15 (𝑦 = 𝑡𝑌 = 𝑡 / 𝑦𝑌)
8180eqeq2d 2189 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → (𝑤 = 𝑌𝑤 = 𝑡 / 𝑦𝑌))
8281anbi2d 464 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)))
83 opeq2 3777 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑡⟩)
8483eqeq1d 2186 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
8582, 84bibi12d 235 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)))
8673, 79, 85cbvral 2699 . . . . . . . . . . 11 (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
87 csbeq1a 3066 . . . . . . . . . . . . . . 15 (𝑥 = 𝑠𝑋 = 𝑠 / 𝑥𝑋)
8887eqeq2d 2189 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → (𝑧 = 𝑋𝑧 = 𝑠 / 𝑥𝑋))
8988anbi1d 465 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
90 opeq1 3776 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → ⟨𝑥, 𝑡⟩ = ⟨𝑠, 𝑡⟩)
9190eqeq1d 2186 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (⟨𝑥, 𝑡⟩ = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9289, 91bibi12d 235 . . . . . . . . . . . 12 (𝑥 = 𝑠 → (((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9392ralbidv 2477 . . . . . . . . . . 11 (𝑥 = 𝑠 → (∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9486, 93bitrid 192 . . . . . . . . . 10 (𝑥 = 𝑠 → (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9564, 72, 94cbvral 2699 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9663, 95bitr4i 187 . . . . . . . 8 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣))
97 eqeq2 2187 . . . . . . . . . . 11 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩))
98 vex 2740 . . . . . . . . . . . 12 𝑥 ∈ V
99 vex 2740 . . . . . . . . . . . 12 𝑦 ∈ V
10098, 99opth 4234 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩ ↔ (𝑥 = 𝑠𝑦 = 𝑡))
10197, 100bitrdi 196 . . . . . . . . . 10 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
102101bibi2d 232 . . . . . . . . 9 (𝑣 = ⟨𝑠, 𝑡⟩ → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
1031022ralbidv 2501 . . . . . . . 8 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
10496, 103bitrid 192 . . . . . . 7 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
105104rexxp 4767 . . . . . 6 (∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
10651, 105sylibr 134 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
107 reu6 2926 . . . . 5 (∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
108106, 107sylibr 134 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
109108ralrimivva 2559 . . 3 (𝜑 → ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
110 eqeq1 2184 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
111 vex 2740 . . . . . . 7 𝑧 ∈ V
112 vex 2740 . . . . . . 7 𝑤 ∈ V
113111, 112opth 4234 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
114110, 113bitrdi 196 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
115114reubidv 2660 . . . 4 (𝑣 = ⟨𝑧, 𝑤⟩ → (∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
116115ralxp 4766 . . 3 (∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
117109, 116sylibr 134 . 2 (𝜑 → ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
118 nfcv 2319 . . . . 5 𝑧𝑋, 𝑌
119 nfcv 2319 . . . . 5 𝑤𝑋, 𝑌
120 nfcsb1v 3090 . . . . . 6 𝑥𝑧 / 𝑥𝑋
121 nfcv 2319 . . . . . 6 𝑥𝑤 / 𝑦𝑌
122120, 121nfop 3792 . . . . 5 𝑥𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
123 nfcv 2319 . . . . . 6 𝑦𝑧 / 𝑥𝑋
124 nfcsb1v 3090 . . . . . 6 𝑦𝑤 / 𝑦𝑌
125123, 124nfop 3792 . . . . 5 𝑦𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
126 csbeq1a 3066 . . . . . 6 (𝑥 = 𝑧𝑋 = 𝑧 / 𝑥𝑋)
127 csbeq1a 3066 . . . . . 6 (𝑦 = 𝑤𝑌 = 𝑤 / 𝑦𝑌)
128 opeq12 3778 . . . . . 6 ((𝑋 = 𝑧 / 𝑥𝑋𝑌 = 𝑤 / 𝑦𝑌) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
129126, 127, 128syl2an 289 . . . . 5 ((𝑥 = 𝑧𝑦 = 𝑤) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
130118, 119, 122, 125, 129cbvmpo 5948 . . . 4 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
131111, 112op1std 6143 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) = 𝑧)
132131csbeq1d 3064 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) / 𝑥𝑋 = 𝑧 / 𝑥𝑋)
133111, 112op2ndd 6144 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) = 𝑤)
134133csbeq1d 3064 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑤 / 𝑦𝑌)
135132, 134opeq12d 3784 . . . . 5 (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
136135mpompt 5961 . . . 4 (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
137130, 136eqtr4i 2201 . . 3 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
138137f1ompt 5663 . 2 ((𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷) ↔ (∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷) ∧ ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
13931, 117, 138sylanbrc 417 1 (𝜑 → (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  wral 2455  wrex 2456  ∃!wreu 2457  csb 3057  cop 3594  cmpt 4061   × cxp 4621  1-1-ontowf1o 5211  cfv 5212  cmpo 5871  1st c1st 6133  2nd c2nd 6134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136
This theorem is referenced by:  xpen  6839
  Copyright terms: Public domain W3C validator