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

Theorem xpf1o 6667
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 5994 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (1st𝑢) ∈ 𝐴)
21adantl 273 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) ∈ 𝐴)
3 xpf1o.1 . . . . . . . 8 (𝜑 → (𝑥𝐴𝑋):𝐴1-1-onto𝐵)
4 eqid 2100 . . . . . . . . 9 (𝑥𝐴𝑋) = (𝑥𝐴𝑋)
54f1ompt 5503 . . . . . . . 8 ((𝑥𝐴𝑋):𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
63, 5sylib 121 . . . . . . 7 (𝜑 → (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
76simpld 111 . . . . . 6 (𝜑 → ∀𝑥𝐴 𝑋𝐵)
87adantr 272 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑥𝐴 𝑋𝐵)
9 nfcsb1v 2985 . . . . . . 7 𝑥(1st𝑢) / 𝑥𝑋
109nfel1 2251 . . . . . 6 𝑥(1st𝑢) / 𝑥𝑋𝐵
11 csbeq1a 2963 . . . . . . 7 (𝑥 = (1st𝑢) → 𝑋 = (1st𝑢) / 𝑥𝑋)
1211eleq1d 2168 . . . . . 6 (𝑥 = (1st𝑢) → (𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
1310, 12rspc 2738 . . . . 5 ((1st𝑢) ∈ 𝐴 → (∀𝑥𝐴 𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
142, 8, 13sylc 62 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) / 𝑥𝑋𝐵)
15 xp2nd 5995 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (2nd𝑢) ∈ 𝐶)
1615adantl 273 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) ∈ 𝐶)
17 xpf1o.2 . . . . . . . 8 (𝜑 → (𝑦𝐶𝑌):𝐶1-1-onto𝐷)
18 eqid 2100 . . . . . . . . 9 (𝑦𝐶𝑌) = (𝑦𝐶𝑌)
1918f1ompt 5503 . . . . . . . 8 ((𝑦𝐶𝑌):𝐶1-1-onto𝐷 ↔ (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2017, 19sylib 121 . . . . . . 7 (𝜑 → (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2120simpld 111 . . . . . 6 (𝜑 → ∀𝑦𝐶 𝑌𝐷)
2221adantr 272 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑦𝐶 𝑌𝐷)
23 nfcsb1v 2985 . . . . . . 7 𝑦(2nd𝑢) / 𝑦𝑌
2423nfel1 2251 . . . . . 6 𝑦(2nd𝑢) / 𝑦𝑌𝐷
25 csbeq1a 2963 . . . . . . 7 (𝑦 = (2nd𝑢) → 𝑌 = (2nd𝑢) / 𝑦𝑌)
2625eleq1d 2168 . . . . . 6 (𝑦 = (2nd𝑢) → (𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2724, 26rspc 2738 . . . . 5 ((2nd𝑢) ∈ 𝐶 → (∀𝑦𝐶 𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2816, 22, 27sylc 62 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) / 𝑦𝑌𝐷)
29 opelxpi 4509 . . . 4 (((1st𝑢) / 𝑥𝑋𝐵(2nd𝑢) / 𝑦𝑌𝐷) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3014, 28, 29syl2anc 406 . . 3 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3130ralrimiva 2464 . 2 (𝜑 → ∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
326simprd 113 . . . . . . . . . 10 (𝜑 → ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋)
3332r19.21bi 2479 . . . . . . . . 9 ((𝜑𝑧𝐵) → ∃!𝑥𝐴 𝑧 = 𝑋)
34 reu6 2826 . . . . . . . . 9 (∃!𝑥𝐴 𝑧 = 𝑋 ↔ ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3533, 34sylib 121 . . . . . . . 8 ((𝜑𝑧𝐵) → ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3620simprd 113 . . . . . . . . . 10 (𝜑 → ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌)
3736r19.21bi 2479 . . . . . . . . 9 ((𝜑𝑤𝐷) → ∃!𝑦𝐶 𝑤 = 𝑌)
38 reu6 2826 . . . . . . . . 9 (∃!𝑦𝐶 𝑤 = 𝑌 ↔ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
3937, 38sylib 121 . . . . . . . 8 ((𝜑𝑤𝐷) → ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
4035, 39anim12dan 570 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
41 reeanv 2558 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) ↔ (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
42 pm4.38 575 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑋𝑥 = 𝑠) ∧ (𝑤 = 𝑌𝑦 = 𝑡)) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4342ex 114 . . . . . . . . . . . . . 14 ((𝑧 = 𝑋𝑥 = 𝑠) → ((𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4443ralimdv 2459 . . . . . . . . . . . . 13 ((𝑧 = 𝑋𝑥 = 𝑠) → (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4544com12 30 . . . . . . . . . . . 12 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4645ralimdv 2459 . . . . . . . . . . 11 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4746impcom 124 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4847reximi 2488 . . . . . . . . 9 (∃𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4948reximi 2488 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5041, 49sylbir 134 . . . . . . 7 ((∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5140, 50syl 14 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
52 vex 2644 . . . . . . . . . . . . . . 15 𝑠 ∈ V
53 vex 2644 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5452, 53op1std 5977 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) = 𝑠)
5554csbeq1d 2961 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) / 𝑥𝑋 = 𝑠 / 𝑥𝑋)
5655eqeq2d 2111 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑧 = (1st𝑢) / 𝑥𝑋𝑧 = 𝑠 / 𝑥𝑋))
5752, 53op2ndd 5978 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) = 𝑡)
5857csbeq1d 2961 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑡 / 𝑦𝑌)
5958eqeq2d 2111 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑤 = (2nd𝑢) / 𝑦𝑌𝑤 = 𝑡 / 𝑦𝑌))
6056, 59anbi12d 460 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → ((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
61 eqeq1 2106 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑢 = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
6260, 61bibi12d 234 . . . . . . . . . 10 (𝑢 = ⟨𝑠, 𝑡⟩ → (((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
6362ralxp 4620 . . . . . . . . 9 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
64 nfv 1476 . . . . . . . . . 10 𝑠𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
65 nfcv 2240 . . . . . . . . . . 11 𝑥𝐶
66 nfcsb1v 2985 . . . . . . . . . . . . . 14 𝑥𝑠 / 𝑥𝑋
6766nfeq2 2252 . . . . . . . . . . . . 13 𝑥 𝑧 = 𝑠 / 𝑥𝑋
68 nfv 1476 . . . . . . . . . . . . 13 𝑥 𝑤 = 𝑡 / 𝑦𝑌
6967, 68nfan 1512 . . . . . . . . . . . 12 𝑥(𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)
70 nfv 1476 . . . . . . . . . . . 12 𝑥𝑠, 𝑡⟩ = 𝑣
7169, 70nfbi 1536 . . . . . . . . . . 11 𝑥((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
7265, 71nfralxy 2430 . . . . . . . . . 10 𝑥𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
73 nfv 1476 . . . . . . . . . . . 12 𝑡((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
74 nfv 1476 . . . . . . . . . . . . . 14 𝑦 𝑧 = 𝑋
75 nfcsb1v 2985 . . . . . . . . . . . . . . 15 𝑦𝑡 / 𝑦𝑌
7675nfeq2 2252 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑡 / 𝑦𝑌
7774, 76nfan 1512 . . . . . . . . . . . . 13 𝑦(𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)
78 nfv 1476 . . . . . . . . . . . . 13 𝑦𝑥, 𝑡⟩ = 𝑣
7977, 78nfbi 1536 . . . . . . . . . . . 12 𝑦((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)
80 csbeq1a 2963 . . . . . . . . . . . . . . 15 (𝑦 = 𝑡𝑌 = 𝑡 / 𝑦𝑌)
8180eqeq2d 2111 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → (𝑤 = 𝑌𝑤 = 𝑡 / 𝑦𝑌))
8281anbi2d 455 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)))
83 opeq2 3653 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑡⟩)
8483eqeq1d 2108 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
8582, 84bibi12d 234 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)))
8673, 79, 85cbvral 2608 . . . . . . . . . . 11 (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
87 csbeq1a 2963 . . . . . . . . . . . . . . 15 (𝑥 = 𝑠𝑋 = 𝑠 / 𝑥𝑋)
8887eqeq2d 2111 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → (𝑧 = 𝑋𝑧 = 𝑠 / 𝑥𝑋))
8988anbi1d 456 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
90 opeq1 3652 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → ⟨𝑥, 𝑡⟩ = ⟨𝑠, 𝑡⟩)
9190eqeq1d 2108 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (⟨𝑥, 𝑡⟩ = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9289, 91bibi12d 234 . . . . . . . . . . . 12 (𝑥 = 𝑠 → (((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9392ralbidv 2396 . . . . . . . . . . 11 (𝑥 = 𝑠 → (∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9486, 93syl5bb 191 . . . . . . . . . 10 (𝑥 = 𝑠 → (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9564, 72, 94cbvral 2608 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9663, 95bitr4i 186 . . . . . . . 8 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣))
97 eqeq2 2109 . . . . . . . . . . 11 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩))
98 vex 2644 . . . . . . . . . . . 12 𝑥 ∈ V
99 vex 2644 . . . . . . . . . . . 12 𝑦 ∈ V
10098, 99opth 4097 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩ ↔ (𝑥 = 𝑠𝑦 = 𝑡))
10197, 100syl6bb 195 . . . . . . . . . 10 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
102101bibi2d 231 . . . . . . . . 9 (𝑣 = ⟨𝑠, 𝑡⟩ → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
1031022ralbidv 2418 . . . . . . . 8 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
10496, 103syl5bb 191 . . . . . . 7 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
105104rexxp 4621 . . . . . 6 (∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
10651, 105sylibr 133 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
107 reu6 2826 . . . . 5 (∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
108106, 107sylibr 133 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
109108ralrimivva 2473 . . 3 (𝜑 → ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
110 eqeq1 2106 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
111 vex 2644 . . . . . . 7 𝑧 ∈ V
112 vex 2644 . . . . . . 7 𝑤 ∈ V
113111, 112opth 4097 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
114110, 113syl6bb 195 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
115114reubidv 2572 . . . 4 (𝑣 = ⟨𝑧, 𝑤⟩ → (∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
116115ralxp 4620 . . 3 (∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
117109, 116sylibr 133 . 2 (𝜑 → ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
118 nfcv 2240 . . . . 5 𝑧𝑋, 𝑌
119 nfcv 2240 . . . . 5 𝑤𝑋, 𝑌
120 nfcsb1v 2985 . . . . . 6 𝑥𝑧 / 𝑥𝑋
121 nfcv 2240 . . . . . 6 𝑥𝑤 / 𝑦𝑌
122120, 121nfop 3668 . . . . 5 𝑥𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
123 nfcv 2240 . . . . . 6 𝑦𝑧 / 𝑥𝑋
124 nfcsb1v 2985 . . . . . 6 𝑦𝑤 / 𝑦𝑌
125123, 124nfop 3668 . . . . 5 𝑦𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
126 csbeq1a 2963 . . . . . 6 (𝑥 = 𝑧𝑋 = 𝑧 / 𝑥𝑋)
127 csbeq1a 2963 . . . . . 6 (𝑦 = 𝑤𝑌 = 𝑤 / 𝑦𝑌)
128 opeq12 3654 . . . . . 6 ((𝑋 = 𝑧 / 𝑥𝑋𝑌 = 𝑤 / 𝑦𝑌) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
129126, 127, 128syl2an 285 . . . . 5 ((𝑥 = 𝑧𝑦 = 𝑤) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
130118, 119, 122, 125, 129cbvmpo 5782 . . . 4 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
131111, 112op1std 5977 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) = 𝑧)
132131csbeq1d 2961 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) / 𝑥𝑋 = 𝑧 / 𝑥𝑋)
133111, 112op2ndd 5978 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) = 𝑤)
134133csbeq1d 2961 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑤 / 𝑦𝑌)
135132, 134opeq12d 3660 . . . . 5 (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
136135mpompt 5795 . . . 4 (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
137130, 136eqtr4i 2123 . . 3 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
138137f1ompt 5503 . 2 ((𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷) ↔ (∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷) ∧ ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
13931, 117, 138sylanbrc 411 1 (𝜑 → (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1299  wcel 1448  wral 2375  wrex 2376  ∃!wreu 2377  csb 2955  cop 3477  cmpt 3929   × cxp 4475  1-1-ontowf1o 5058  cfv 5059  cmpo 5708  1st c1st 5967  2nd c2nd 5968
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293
This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-iun 3762  df-br 3876  df-opab 3930  df-mpt 3931  df-id 4153  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067  df-oprab 5710  df-mpo 5711  df-1st 5969  df-2nd 5970
This theorem is referenced by:  xpen  6668
  Copyright terms: Public domain W3C validator