Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  f1od2 Structured version   Visualization version   GIF version

Theorem f1od2 29342
Description: Describe an implicit one-to-one onto function of two variables. (Contributed by Thierry Arnoux, 17-Aug-2017.)
Hypotheses
Ref Expression
f1od2.1 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
f1od2.2 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶𝑊)
f1od2.3 ((𝜑𝑧𝐷) → (𝐼𝑋𝐽𝑌))
f1od2.4 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
Assertion
Ref Expression
f1od2 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑧,𝐶   𝑥,𝐷,𝑦,𝑧   𝑥,𝐼,𝑦   𝑥,𝐽,𝑦   𝜑,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦,𝑧)   𝐼(𝑧)   𝐽(𝑧)   𝑊(𝑥,𝑦,𝑧)   𝑋(𝑥,𝑦,𝑧)   𝑌(𝑥,𝑦,𝑧)

Proof of Theorem f1od2
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 f1od2.2 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶𝑊)
21ralrimivva 2965 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝐶𝑊)
3 f1od2.1 . . . 4 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
43fnmpt2 7183 . . 3 (∀𝑥𝐴𝑦𝐵 𝐶𝑊𝐹 Fn (𝐴 × 𝐵))
52, 4syl 17 . 2 (𝜑𝐹 Fn (𝐴 × 𝐵))
6 f1od2.3 . . . . . 6 ((𝜑𝑧𝐷) → (𝐼𝑋𝐽𝑌))
7 opelxpi 5108 . . . . . 6 ((𝐼𝑋𝐽𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
86, 7syl 17 . . . . 5 ((𝜑𝑧𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
98ralrimiva 2960 . . . 4 (𝜑 → ∀𝑧𝐷𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10 eqid 2621 . . . . 5 (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩)
1110fnmpt 5977 . . . 4 (∀𝑧𝐷𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
129, 11syl 17 . . 3 (𝜑 → (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13 elxp7 7146 . . . . . . . 8 (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)))
1413anbi1i 730 . . . . . . 7 ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ ((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
15 anass 680 . . . . . . . . 9 (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑎 ∈ (V × V) ∧ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)))
16 f1od2.4 . . . . . . . . . . . . 13 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
1716sbcbidv 3472 . . . . . . . . . . . 12 (𝜑 → ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
1817sbcbidv 3472 . . . . . . . . . . 11 (𝜑 → ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
19 sbcan 3460 . . . . . . . . . . . . . 14 ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ∧ [(2nd𝑎) / 𝑦]𝑧 = 𝐶))
20 sbcan 3460 . . . . . . . . . . . . . . . 16 ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ↔ ([(2nd𝑎) / 𝑦]𝑥𝐴[(2nd𝑎) / 𝑦]𝑦𝐵))
21 fvex 6158 . . . . . . . . . . . . . . . . . 18 (2nd𝑎) ∈ V
22 sbcg 3485 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑥𝐴𝑥𝐴))
2321, 22ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑥𝐴𝑥𝐴)
24 sbcel1v 3477 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑦𝐵 ↔ (2nd𝑎) ∈ 𝐵)
2523, 24anbi12i 732 . . . . . . . . . . . . . . . 16 (([(2nd𝑎) / 𝑦]𝑥𝐴[(2nd𝑎) / 𝑦]𝑦𝐵) ↔ (𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵))
2620, 25bitri 264 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵))
27 sbceq2g 3962 . . . . . . . . . . . . . . . 16 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑎) / 𝑦𝐶))
2821, 27ax-mp 5 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑎) / 𝑦𝐶)
2926, 28anbi12i 732 . . . . . . . . . . . . . 14 (([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ∧ [(2nd𝑎) / 𝑦]𝑧 = 𝐶) ↔ ((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
3019, 29bitri 264 . . . . . . . . . . . . 13 ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
3130sbcbii 3473 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(1st𝑎) / 𝑥]((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
32 sbcan 3460 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥]((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶) ↔ ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ [(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶))
33 sbcan 3460 . . . . . . . . . . . . . 14 ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ↔ ([(1st𝑎) / 𝑥]𝑥𝐴[(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵))
34 sbcel1v 3477 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥]𝑥𝐴 ↔ (1st𝑎) ∈ 𝐴)
35 fvex 6158 . . . . . . . . . . . . . . . 16 (1st𝑎) ∈ V
36 sbcg 3485 . . . . . . . . . . . . . . . 16 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵 ↔ (2nd𝑎) ∈ 𝐵))
3735, 36ax-mp 5 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵 ↔ (2nd𝑎) ∈ 𝐵)
3834, 37anbi12i 732 . . . . . . . . . . . . . 14 (([(1st𝑎) / 𝑥]𝑥𝐴[(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵) ↔ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵))
3933, 38bitri 264 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ↔ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵))
40 sbceq2g 3962 . . . . . . . . . . . . . 14 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
4135, 40ax-mp 5 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)
4239, 41anbi12i 732 . . . . . . . . . . . 12 (([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ [(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶) ↔ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
4331, 32, 423bitri 286 . . . . . . . . . . 11 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
44 sbcan 3460 . . . . . . . . . . . . . 14 ([(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ ([(2nd𝑎) / 𝑦]𝑧𝐷[(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽)))
45 sbcg 3485 . . . . . . . . . . . . . . . 16 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑧𝐷𝑧𝐷))
4621, 45ax-mp 5 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦]𝑧𝐷𝑧𝐷)
47 sbcan 3460 . . . . . . . . . . . . . . . 16 ([(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽) ↔ ([(2nd𝑎) / 𝑦]𝑥 = 𝐼[(2nd𝑎) / 𝑦]𝑦 = 𝐽))
48 sbcg 3485 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑥 = 𝐼𝑥 = 𝐼))
4921, 48ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑥 = 𝐼𝑥 = 𝐼)
50 sbceq1g 3960 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑦 = 𝐽(2nd𝑎) / 𝑦𝑦 = 𝐽))
5121, 50ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([(2nd𝑎) / 𝑦]𝑦 = 𝐽(2nd𝑎) / 𝑦𝑦 = 𝐽)
52 csbvarg 3975 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑎) ∈ V → (2nd𝑎) / 𝑦𝑦 = (2nd𝑎))
5321, 52ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (2nd𝑎) / 𝑦𝑦 = (2nd𝑎)
5453eqeq1i 2626 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) / 𝑦𝑦 = 𝐽 ↔ (2nd𝑎) = 𝐽)
5551, 54bitri 264 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2nd𝑎) = 𝐽)
5649, 55anbi12i 732 . . . . . . . . . . . . . . . 16 (([(2nd𝑎) / 𝑦]𝑥 = 𝐼[(2nd𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽))
5747, 56bitri 264 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽))
5846, 57anbi12i 732 . . . . . . . . . . . . . 14 (([(2nd𝑎) / 𝑦]𝑧𝐷[(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
5944, 58bitri 264 . . . . . . . . . . . . 13 ([(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
6059sbcbii 3473 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ [(1st𝑎) / 𝑥](𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
61 sbcan 3460 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥](𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)) ↔ ([(1st𝑎) / 𝑥]𝑧𝐷[(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
62 sbcg 3485 . . . . . . . . . . . . . 14 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑧𝐷𝑧𝐷))
6335, 62ax-mp 5 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥]𝑧𝐷𝑧𝐷)
64 sbcan 3460 . . . . . . . . . . . . . 14 ([(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽) ↔ ([(1st𝑎) / 𝑥]𝑥 = 𝐼[(1st𝑎) / 𝑥](2nd𝑎) = 𝐽))
65 sbceq1g 3960 . . . . . . . . . . . . . . . . 17 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑥 = 𝐼(1st𝑎) / 𝑥𝑥 = 𝐼))
6635, 65ax-mp 5 . . . . . . . . . . . . . . . 16 ([(1st𝑎) / 𝑥]𝑥 = 𝐼(1st𝑎) / 𝑥𝑥 = 𝐼)
67 csbvarg 3975 . . . . . . . . . . . . . . . . . 18 ((1st𝑎) ∈ V → (1st𝑎) / 𝑥𝑥 = (1st𝑎))
6835, 67ax-mp 5 . . . . . . . . . . . . . . . . 17 (1st𝑎) / 𝑥𝑥 = (1st𝑎)
6968eqeq1i 2626 . . . . . . . . . . . . . . . 16 ((1st𝑎) / 𝑥𝑥 = 𝐼 ↔ (1st𝑎) = 𝐼)
7066, 69bitri 264 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1st𝑎) = 𝐼)
71 sbcg 3485 . . . . . . . . . . . . . . . 16 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥](2nd𝑎) = 𝐽 ↔ (2nd𝑎) = 𝐽))
7235, 71ax-mp 5 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥](2nd𝑎) = 𝐽 ↔ (2nd𝑎) = 𝐽)
7370, 72anbi12i 732 . . . . . . . . . . . . . 14 (([(1st𝑎) / 𝑥]𝑥 = 𝐼[(1st𝑎) / 𝑥](2nd𝑎) = 𝐽) ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))
7464, 73bitri 264 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽) ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))
7563, 74anbi12i 732 . . . . . . . . . . . 12 (([(1st𝑎) / 𝑥]𝑧𝐷[(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
7660, 61, 753bitri 286 . . . . . . . . . . 11 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
7718, 43, 763bitr3g 302 . . . . . . . . . 10 (𝜑 → ((((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
7877anbi2d 739 . . . . . . . . 9 (𝜑 → ((𝑎 ∈ (V × V) ∧ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))))
7915, 78syl5bb 272 . . . . . . . 8 (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))))
80 xpss 5187 . . . . . . . . . . . 12 (𝑋 × 𝑌) ⊆ (V × V)
81 simprr 795 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
828adantrr 752 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8381, 82eqeltrd 2698 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
8480, 83sseldi 3581 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
8584ex 450 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
8685pm4.71rd 666 . . . . . . . . 9 (𝜑 → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩))))
87 eqop 7153 . . . . . . . . . . 11 (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
8887anbi2d 739 . . . . . . . . . 10 (𝑎 ∈ (V × V) → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
8988pm5.32i 668 . . . . . . . . 9 ((𝑎 ∈ (V × V) ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
9086, 89syl6rbb 277 . . . . . . . 8 (𝜑 → ((𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
9179, 90bitrd 268 . . . . . . 7 (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
9214, 91syl5bb 272 . . . . . 6 (𝜑 → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
9392opabbidv 4678 . . . . 5 (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)})
94 df-mpt2 6609 . . . . . . . 8 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
953, 94eqtri 2643 . . . . . . 7 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
9695cnveqi 5257 . . . . . 6 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
97 nfv 1840 . . . . . . . 8 𝑥 𝑎 ∈ (𝐴 × 𝐵)
98 nfcsb1v 3530 . . . . . . . . 9 𝑥(1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
9998nfeq2 2776 . . . . . . . 8 𝑥 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
10097, 99nfan 1825 . . . . . . 7 𝑥(𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)
101 nfv 1840 . . . . . . . 8 𝑦 𝑎 ∈ (𝐴 × 𝐵)
102 nfcv 2761 . . . . . . . . . 10 𝑦(1st𝑎)
103 nfcsb1v 3530 . . . . . . . . . 10 𝑦(2nd𝑎) / 𝑦𝐶
104102, 103nfcsb 3532 . . . . . . . . 9 𝑦(1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
105104nfeq2 2776 . . . . . . . 8 𝑦 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
106101, 105nfan 1825 . . . . . . 7 𝑦(𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)
107 eleq1 2686 . . . . . . . . 9 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵)))
108 opelxp 5106 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ↔ (𝑥𝐴𝑦𝐵))
109107, 108syl6bb 276 . . . . . . . 8 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑥𝐴𝑦𝐵)))
110 csbopeq1a 7166 . . . . . . . . 9 (𝑎 = ⟨𝑥, 𝑦⟩ → (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶 = 𝐶)
111110eqeq2d 2631 . . . . . . . 8 (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶𝑧 = 𝐶))
112109, 111anbi12d 746 . . . . . . 7 (𝑎 = ⟨𝑥, 𝑦⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)))
113 xpss 5187 . . . . . . . . 9 (𝐴 × 𝐵) ⊆ (V × V)
114113sseli 3579 . . . . . . . 8 (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
115114adantr 481 . . . . . . 7 ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) → 𝑎 ∈ (V × V))
116100, 106, 112, 115cnvoprab 29341 . . . . . 6 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)}
11796, 116eqtri 2643 . . . . 5 𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)}
118 df-mpt 4675 . . . . 5 (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)}
11993, 117, 1183eqtr4g 2680 . . . 4 (𝜑𝐹 = (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩))
120119fneq1d 5939 . . 3 (𝜑 → (𝐹 Fn 𝐷 ↔ (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
12112, 120mpbird 247 . 2 (𝜑𝐹 Fn 𝐷)
122 dff1o4 6102 . 2 (𝐹:(𝐴 × 𝐵)–1-1-onto𝐷 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ 𝐹 Fn 𝐷))
1235, 121, 122sylanbrc 697 1 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  Vcvv 3186  [wsbc 3417  csb 3514  cop 4154  {copab 4672  cmpt 4673   × cxp 5072  ccnv 5073   Fn wfn 5842  1-1-ontowf1o 5846  cfv 5847  {coprab 6605  cmpt2 6606  1st c1st 7111  2nd c2nd 7112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114
This theorem is referenced by:  oddpwdc  30197
  Copyright terms: Public domain W3C validator