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

Theorem xpf1o 9139
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 8007 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (1st𝑢) ∈ 𝐴)
21adantl 483 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) ∈ 𝐴)
3 xpf1o.1 . . . . . . . 8 (𝜑 → (𝑥𝐴𝑋):𝐴1-1-onto𝐵)
4 eqid 2733 . . . . . . . . 9 (𝑥𝐴𝑋) = (𝑥𝐴𝑋)
54f1ompt 7111 . . . . . . . 8 ((𝑥𝐴𝑋):𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
63, 5sylib 217 . . . . . . 7 (𝜑 → (∀𝑥𝐴 𝑋𝐵 ∧ ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋))
76simpld 496 . . . . . 6 (𝜑 → ∀𝑥𝐴 𝑋𝐵)
87adantr 482 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑥𝐴 𝑋𝐵)
9 nfcsb1v 3919 . . . . . . 7 𝑥(1st𝑢) / 𝑥𝑋
109nfel1 2920 . . . . . 6 𝑥(1st𝑢) / 𝑥𝑋𝐵
11 csbeq1a 3908 . . . . . . 7 (𝑥 = (1st𝑢) → 𝑋 = (1st𝑢) / 𝑥𝑋)
1211eleq1d 2819 . . . . . 6 (𝑥 = (1st𝑢) → (𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
1310, 12rspc 3601 . . . . 5 ((1st𝑢) ∈ 𝐴 → (∀𝑥𝐴 𝑋𝐵(1st𝑢) / 𝑥𝑋𝐵))
142, 8, 13sylc 65 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (1st𝑢) / 𝑥𝑋𝐵)
15 xp2nd 8008 . . . . . 6 (𝑢 ∈ (𝐴 × 𝐶) → (2nd𝑢) ∈ 𝐶)
1615adantl 483 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) ∈ 𝐶)
17 xpf1o.2 . . . . . . . 8 (𝜑 → (𝑦𝐶𝑌):𝐶1-1-onto𝐷)
18 eqid 2733 . . . . . . . . 9 (𝑦𝐶𝑌) = (𝑦𝐶𝑌)
1918f1ompt 7111 . . . . . . . 8 ((𝑦𝐶𝑌):𝐶1-1-onto𝐷 ↔ (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2017, 19sylib 217 . . . . . . 7 (𝜑 → (∀𝑦𝐶 𝑌𝐷 ∧ ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌))
2120simpld 496 . . . . . 6 (𝜑 → ∀𝑦𝐶 𝑌𝐷)
2221adantr 482 . . . . 5 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ∀𝑦𝐶 𝑌𝐷)
23 nfcsb1v 3919 . . . . . . 7 𝑦(2nd𝑢) / 𝑦𝑌
2423nfel1 2920 . . . . . 6 𝑦(2nd𝑢) / 𝑦𝑌𝐷
25 csbeq1a 3908 . . . . . . 7 (𝑦 = (2nd𝑢) → 𝑌 = (2nd𝑢) / 𝑦𝑌)
2625eleq1d 2819 . . . . . 6 (𝑦 = (2nd𝑢) → (𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2724, 26rspc 3601 . . . . 5 ((2nd𝑢) ∈ 𝐶 → (∀𝑦𝐶 𝑌𝐷(2nd𝑢) / 𝑦𝑌𝐷))
2816, 22, 27sylc 65 . . . 4 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → (2nd𝑢) / 𝑦𝑌𝐷)
2914, 28opelxpd 5716 . . 3 ((𝜑𝑢 ∈ (𝐴 × 𝐶)) → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
3029ralrimiva 3147 . 2 (𝜑 → ∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷))
316simprd 497 . . . . . . . . . 10 (𝜑 → ∀𝑧𝐵 ∃!𝑥𝐴 𝑧 = 𝑋)
3231r19.21bi 3249 . . . . . . . . 9 ((𝜑𝑧𝐵) → ∃!𝑥𝐴 𝑧 = 𝑋)
33 reu6 3723 . . . . . . . . 9 (∃!𝑥𝐴 𝑧 = 𝑋 ↔ ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3432, 33sylib 217 . . . . . . . 8 ((𝜑𝑧𝐵) → ∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠))
3520simprd 497 . . . . . . . . . 10 (𝜑 → ∀𝑤𝐷 ∃!𝑦𝐶 𝑤 = 𝑌)
3635r19.21bi 3249 . . . . . . . . 9 ((𝜑𝑤𝐷) → ∃!𝑦𝐶 𝑤 = 𝑌)
37 reu6 3723 . . . . . . . . 9 (∃!𝑦𝐶 𝑤 = 𝑌 ↔ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
3836, 37sylib 217 . . . . . . . 8 ((𝜑𝑤𝐷) → ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡))
3934, 38anim12dan 620 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
40 reeanv 3227 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) ↔ (∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)))
41 pm4.38 637 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑋𝑥 = 𝑠) ∧ (𝑤 = 𝑌𝑦 = 𝑡)) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4241ex 414 . . . . . . . . . . . . . 14 ((𝑧 = 𝑋𝑥 = 𝑠) → ((𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4342ralimdv 3170 . . . . . . . . . . . . 13 ((𝑧 = 𝑋𝑥 = 𝑠) → (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4443com12 32 . . . . . . . . . . . 12 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → ((𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4544ralimdv 3170 . . . . . . . . . . 11 (∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡) → (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
4645impcom 409 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4746reximi 3085 . . . . . . . . 9 (∃𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4847reximi 3085 . . . . . . . 8 (∃𝑠𝐴𝑡𝐶 (∀𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∀𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
4940, 48sylbir 234 . . . . . . 7 ((∃𝑠𝐴𝑥𝐴 (𝑧 = 𝑋𝑥 = 𝑠) ∧ ∃𝑡𝐶𝑦𝐶 (𝑤 = 𝑌𝑦 = 𝑡)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
5039, 49syl 17 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
51 vex 3479 . . . . . . . . . . . . . . 15 𝑠 ∈ V
52 vex 3479 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5351, 52op1std 7985 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) = 𝑠)
5453csbeq1d 3898 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (1st𝑢) / 𝑥𝑋 = 𝑠 / 𝑥𝑋)
5554eqeq2d 2744 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑧 = (1st𝑢) / 𝑥𝑋𝑧 = 𝑠 / 𝑥𝑋))
5651, 52op2ndd 7986 . . . . . . . . . . . . . 14 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) = 𝑡)
5756csbeq1d 3898 . . . . . . . . . . . . 13 (𝑢 = ⟨𝑠, 𝑡⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑡 / 𝑦𝑌)
5857eqeq2d 2744 . . . . . . . . . . . 12 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑤 = (2nd𝑢) / 𝑦𝑌𝑤 = 𝑡 / 𝑦𝑌))
5955, 58anbi12d 632 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → ((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
60 eqeq1 2737 . . . . . . . . . . 11 (𝑢 = ⟨𝑠, 𝑡⟩ → (𝑢 = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
6159, 60bibi12d 346 . . . . . . . . . 10 (𝑢 = ⟨𝑠, 𝑡⟩ → (((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
6261ralxp 5842 . . . . . . . . 9 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
63 nfv 1918 . . . . . . . . . 10 𝑠𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
64 nfcv 2904 . . . . . . . . . . 11 𝑥𝐶
65 nfcsb1v 3919 . . . . . . . . . . . . . 14 𝑥𝑠 / 𝑥𝑋
6665nfeq2 2921 . . . . . . . . . . . . 13 𝑥 𝑧 = 𝑠 / 𝑥𝑋
67 nfv 1918 . . . . . . . . . . . . 13 𝑥 𝑤 = 𝑡 / 𝑦𝑌
6866, 67nfan 1903 . . . . . . . . . . . 12 𝑥(𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)
69 nfv 1918 . . . . . . . . . . . 12 𝑥𝑠, 𝑡⟩ = 𝑣
7068, 69nfbi 1907 . . . . . . . . . . 11 𝑥((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
7164, 70nfralw 3309 . . . . . . . . . 10 𝑥𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)
72 nfv 1918 . . . . . . . . . . . 12 𝑡((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣)
73 nfv 1918 . . . . . . . . . . . . . 14 𝑦 𝑧 = 𝑋
74 nfcsb1v 3919 . . . . . . . . . . . . . . 15 𝑦𝑡 / 𝑦𝑌
7574nfeq2 2921 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑡 / 𝑦𝑌
7673, 75nfan 1903 . . . . . . . . . . . . 13 𝑦(𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)
77 nfv 1918 . . . . . . . . . . . . 13 𝑦𝑥, 𝑡⟩ = 𝑣
7876, 77nfbi 1907 . . . . . . . . . . . 12 𝑦((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)
79 csbeq1a 3908 . . . . . . . . . . . . . . 15 (𝑦 = 𝑡𝑌 = 𝑡 / 𝑦𝑌)
8079eqeq2d 2744 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → (𝑤 = 𝑌𝑤 = 𝑡 / 𝑦𝑌))
8180anbi2d 630 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌)))
82 opeq2 4875 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑡⟩)
8382eqeq1d 2735 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
8481, 83bibi12d 346 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣)))
8572, 78, 84cbvralw 3304 . . . . . . . . . . 11 (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣))
86 csbeq1a 3908 . . . . . . . . . . . . . . 15 (𝑥 = 𝑠𝑋 = 𝑠 / 𝑥𝑋)
8786eqeq2d 2744 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → (𝑧 = 𝑋𝑧 = 𝑠 / 𝑥𝑋))
8887anbi1d 631 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ (𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌)))
89 opeq1 4874 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → ⟨𝑥, 𝑡⟩ = ⟨𝑠, 𝑡⟩)
9089eqeq1d 2735 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (⟨𝑥, 𝑡⟩ = 𝑣 ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9188, 90bibi12d 346 . . . . . . . . . . . 12 (𝑥 = 𝑠 → (((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9291ralbidv 3178 . . . . . . . . . . 11 (𝑥 = 𝑠 → (∀𝑡𝐶 ((𝑧 = 𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑥, 𝑡⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9385, 92bitrid 283 . . . . . . . . . 10 (𝑥 = 𝑠 → (∀𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣)))
9463, 71, 93cbvralw 3304 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑠𝐴𝑡𝐶 ((𝑧 = 𝑠 / 𝑥𝑋𝑤 = 𝑡 / 𝑦𝑌) ↔ ⟨𝑠, 𝑡⟩ = 𝑣))
9562, 94bitr4i 278 . . . . . . . 8 (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣))
96 eqeq2 2745 . . . . . . . . . . 11 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩))
97 vex 3479 . . . . . . . . . . . 12 𝑥 ∈ V
98 vex 3479 . . . . . . . . . . . 12 𝑦 ∈ V
9997, 98opth 5477 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = ⟨𝑠, 𝑡⟩ ↔ (𝑥 = 𝑠𝑦 = 𝑡))
10096, 99bitrdi 287 . . . . . . . . . 10 (𝑣 = ⟨𝑠, 𝑡⟩ → (⟨𝑥, 𝑦⟩ = 𝑣 ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
101100bibi2d 343 . . . . . . . . 9 (𝑣 = ⟨𝑠, 𝑡⟩ → (((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
1021012ralbidv 3219 . . . . . . . 8 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ ⟨𝑥, 𝑦⟩ = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
10395, 102bitrid 283 . . . . . . 7 (𝑣 = ⟨𝑠, 𝑡⟩ → (∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∀𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡))))
104103rexxp 5843 . . . . . 6 (∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣) ↔ ∃𝑠𝐴𝑡𝐶𝑥𝐴𝑦𝐶 ((𝑧 = 𝑋𝑤 = 𝑌) ↔ (𝑥 = 𝑠𝑦 = 𝑡)))
10550, 104sylibr 233 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
106 reu6 3723 . . . . 5 (∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ ∃𝑣 ∈ (𝐴 × 𝐶)∀𝑢 ∈ (𝐴 × 𝐶)((𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌) ↔ 𝑢 = 𝑣))
107105, 106sylibr 233 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐷)) → ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
108107ralrimivva 3201 . . 3 (𝜑 → ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
109 eqeq1 2737 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
110 vex 3479 . . . . . . 7 𝑧 ∈ V
111 vex 3479 . . . . . . 7 𝑤 ∈ V
112110, 111opth 5477 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
113109, 112bitrdi 287 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ (𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
114113reubidv 3395 . . . 4 (𝑣 = ⟨𝑧, 𝑤⟩ → (∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌)))
115114ralxp 5842 . . 3 (∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ↔ ∀𝑧𝐵𝑤𝐷 ∃!𝑢 ∈ (𝐴 × 𝐶)(𝑧 = (1st𝑢) / 𝑥𝑋𝑤 = (2nd𝑢) / 𝑦𝑌))
116108, 115sylibr 233 . 2 (𝜑 → ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
117 nfcv 2904 . . . . 5 𝑧𝑋, 𝑌
118 nfcv 2904 . . . . 5 𝑤𝑋, 𝑌
119 nfcsb1v 3919 . . . . . 6 𝑥𝑧 / 𝑥𝑋
120 nfcv 2904 . . . . . 6 𝑥𝑤 / 𝑦𝑌
121119, 120nfop 4890 . . . . 5 𝑥𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
122 nfcv 2904 . . . . . 6 𝑦𝑧 / 𝑥𝑋
123 nfcsb1v 3919 . . . . . 6 𝑦𝑤 / 𝑦𝑌
124122, 123nfop 4890 . . . . 5 𝑦𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌
125 csbeq1a 3908 . . . . . 6 (𝑥 = 𝑧𝑋 = 𝑧 / 𝑥𝑋)
126 csbeq1a 3908 . . . . . 6 (𝑦 = 𝑤𝑌 = 𝑤 / 𝑦𝑌)
127 opeq12 4876 . . . . . 6 ((𝑋 = 𝑧 / 𝑥𝑋𝑌 = 𝑤 / 𝑦𝑌) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
128125, 126, 127syl2an 597 . . . . 5 ((𝑥 = 𝑧𝑦 = 𝑤) → ⟨𝑋, 𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
129117, 118, 121, 124, 128cbvmpo 7503 . . . 4 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
130110, 111op1std 7985 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) = 𝑧)
131130csbeq1d 3898 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (1st𝑢) / 𝑥𝑋 = 𝑧 / 𝑥𝑋)
132110, 111op2ndd 7986 . . . . . . 7 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) = 𝑤)
133132csbeq1d 3898 . . . . . 6 (𝑢 = ⟨𝑧, 𝑤⟩ → (2nd𝑢) / 𝑦𝑌 = 𝑤 / 𝑦𝑌)
134131, 133opeq12d 4882 . . . . 5 (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ = ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
135134mpompt 7522 . . . 4 (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩) = (𝑧𝐴, 𝑤𝐶 ↦ ⟨𝑧 / 𝑥𝑋, 𝑤 / 𝑦𝑌⟩)
136129, 135eqtr4i 2764 . . 3 (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩) = (𝑢 ∈ (𝐴 × 𝐶) ↦ ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩)
137136f1ompt 7111 . 2 ((𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷) ↔ (∀𝑢 ∈ (𝐴 × 𝐶)⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩ ∈ (𝐵 × 𝐷) ∧ ∀𝑣 ∈ (𝐵 × 𝐷)∃!𝑢 ∈ (𝐴 × 𝐶)𝑣 = ⟨(1st𝑢) / 𝑥𝑋, (2nd𝑢) / 𝑦𝑌⟩))
13830, 116, 137sylanbrc 584 1 (𝜑 → (𝑥𝐴, 𝑦𝐶 ↦ ⟨𝑋, 𝑌⟩):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  wrex 3071  ∃!wreu 3375  csb 3894  cop 4635  cmpt 5232   × cxp 5675  1-1-ontowf1o 6543  cfv 6544  cmpo 7411  1st c1st 7973  2nd c2nd 7974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976
This theorem is referenced by:  infxpenc  10013  pwfseqlem5  10658
  Copyright terms: Public domain W3C validator