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 30468
Description: Sufficient condition for a binary function expressed in maps-to notation to be bijective. (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 variables 𝑖 𝑎 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1od2.2 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶𝑊)
21ralrimivva 3186 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝐶𝑊)
3 f1od2.1 . . . 4 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
43fnmpo 7762 . . 3 (∀𝑥𝐴𝑦𝐵 𝐶𝑊𝐹 Fn (𝐴 × 𝐵))
52, 4syl 17 . 2 (𝜑𝐹 Fn (𝐴 × 𝐵))
6 f1od2.3 . . . . . 6 ((𝜑𝑧𝐷) → (𝐼𝑋𝐽𝑌))
7 opelxpi 5579 . . . . . 6 ((𝐼𝑋𝐽𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
86, 7syl 17 . . . . 5 ((𝜑𝑧𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
98ralrimiva 3177 . . . 4 (𝜑 → ∀𝑧𝐷𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10 eqid 2824 . . . . 5 (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩)
1110fnmpt 6477 . . . 4 (∀𝑧𝐷𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
129, 11syl 17 . . 3 (𝜑 → (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13 elxp7 7719 . . . . . . . 8 (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)))
1413anbi1i 626 . . . . . . 7 ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ ((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
15 anass 472 . . . . . . . . 9 (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑎 ∈ (V × V) ∧ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)))
16 f1od2.4 . . . . . . . . . . . . 13 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
1716sbcbidv 3812 . . . . . . . . . . . 12 (𝜑 → ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
1817sbcbidv 3812 . . . . . . . . . . 11 (𝜑 → ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
19 sbcan 3806 . . . . . . . . . . . . . 14 ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ∧ [(2nd𝑎) / 𝑦]𝑧 = 𝐶))
20 sbcan 3806 . . . . . . . . . . . . . . . 16 ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ↔ ([(2nd𝑎) / 𝑦]𝑥𝐴[(2nd𝑎) / 𝑦]𝑦𝐵))
21 fvex 6674 . . . . . . . . . . . . . . . . . 18 (2nd𝑎) ∈ V
22 sbcg 3831 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑥𝐴𝑥𝐴))
2321, 22ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑥𝐴𝑥𝐴)
24 sbcel1v 3824 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑦𝐵 ↔ (2nd𝑎) ∈ 𝐵)
2523, 24anbi12i 629 . . . . . . . . . . . . . . . 16 (([(2nd𝑎) / 𝑦]𝑥𝐴[(2nd𝑎) / 𝑦]𝑦𝐵) ↔ (𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵))
2620, 25bitri 278 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵))
27 sbceq2g 4351 . . . . . . . . . . . . . . . 16 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑎) / 𝑦𝐶))
2821, 27ax-mp 5 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑎) / 𝑦𝐶)
2926, 28anbi12i 629 . . . . . . . . . . . . . 14 (([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ∧ [(2nd𝑎) / 𝑦]𝑧 = 𝐶) ↔ ((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
3019, 29bitri 278 . . . . . . . . . . . . 13 ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
3130sbcbii 3814 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(1st𝑎) / 𝑥]((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
32 sbcan 3806 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥]((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶) ↔ ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ [(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶))
33 sbcan 3806 . . . . . . . . . . . . . 14 ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ↔ ([(1st𝑎) / 𝑥]𝑥𝐴[(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵))
34 sbcel1v 3824 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥]𝑥𝐴 ↔ (1st𝑎) ∈ 𝐴)
35 fvex 6674 . . . . . . . . . . . . . . . 16 (1st𝑎) ∈ V
36 sbcg 3831 . . . . . . . . . . . . . . . 16 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵 ↔ (2nd𝑎) ∈ 𝐵))
3735, 36ax-mp 5 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵 ↔ (2nd𝑎) ∈ 𝐵)
3834, 37anbi12i 629 . . . . . . . . . . . . . 14 (([(1st𝑎) / 𝑥]𝑥𝐴[(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵) ↔ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵))
3933, 38bitri 278 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ↔ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵))
40 sbceq2g 4351 . . . . . . . . . . . . . 14 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
4135, 40ax-mp 5 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)
4239, 41anbi12i 629 . . . . . . . . . . . 12 (([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ [(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶) ↔ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
4331, 32, 423bitri 300 . . . . . . . . . . 11 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
44 sbcan 3806 . . . . . . . . . . . . . 14 ([(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ ([(2nd𝑎) / 𝑦]𝑧𝐷[(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽)))
45 sbcg 3831 . . . . . . . . . . . . . . . 16 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑧𝐷𝑧𝐷))
4621, 45ax-mp 5 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦]𝑧𝐷𝑧𝐷)
47 sbcan 3806 . . . . . . . . . . . . . . . 16 ([(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽) ↔ ([(2nd𝑎) / 𝑦]𝑥 = 𝐼[(2nd𝑎) / 𝑦]𝑦 = 𝐽))
48 sbcg 3831 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑥 = 𝐼𝑥 = 𝐼))
4921, 48ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑥 = 𝐼𝑥 = 𝐼)
50 sbceq1g 4349 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑦 = 𝐽(2nd𝑎) / 𝑦𝑦 = 𝐽))
5121, 50ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([(2nd𝑎) / 𝑦]𝑦 = 𝐽(2nd𝑎) / 𝑦𝑦 = 𝐽)
5221csbvargi 4367 . . . . . . . . . . . . . . . . . . 19 (2nd𝑎) / 𝑦𝑦 = (2nd𝑎)
5352eqeq1i 2829 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) / 𝑦𝑦 = 𝐽 ↔ (2nd𝑎) = 𝐽)
5451, 53bitri 278 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2nd𝑎) = 𝐽)
5549, 54anbi12i 629 . . . . . . . . . . . . . . . 16 (([(2nd𝑎) / 𝑦]𝑥 = 𝐼[(2nd𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽))
5647, 55bitri 278 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽))
5746, 56anbi12i 629 . . . . . . . . . . . . . 14 (([(2nd𝑎) / 𝑦]𝑧𝐷[(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
5844, 57bitri 278 . . . . . . . . . . . . 13 ([(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
5958sbcbii 3814 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ [(1st𝑎) / 𝑥](𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
60 sbcan 3806 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥](𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)) ↔ ([(1st𝑎) / 𝑥]𝑧𝐷[(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
61 sbcg 3831 . . . . . . . . . . . . . 14 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑧𝐷𝑧𝐷))
6235, 61ax-mp 5 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥]𝑧𝐷𝑧𝐷)
63 sbcan 3806 . . . . . . . . . . . . . 14 ([(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽) ↔ ([(1st𝑎) / 𝑥]𝑥 = 𝐼[(1st𝑎) / 𝑥](2nd𝑎) = 𝐽))
64 sbceq1g 4349 . . . . . . . . . . . . . . . . 17 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑥 = 𝐼(1st𝑎) / 𝑥𝑥 = 𝐼))
6535, 64ax-mp 5 . . . . . . . . . . . . . . . 16 ([(1st𝑎) / 𝑥]𝑥 = 𝐼(1st𝑎) / 𝑥𝑥 = 𝐼)
6635csbvargi 4367 . . . . . . . . . . . . . . . . 17 (1st𝑎) / 𝑥𝑥 = (1st𝑎)
6766eqeq1i 2829 . . . . . . . . . . . . . . . 16 ((1st𝑎) / 𝑥𝑥 = 𝐼 ↔ (1st𝑎) = 𝐼)
6865, 67bitri 278 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1st𝑎) = 𝐼)
69 sbcg 3831 . . . . . . . . . . . . . . . 16 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥](2nd𝑎) = 𝐽 ↔ (2nd𝑎) = 𝐽))
7035, 69ax-mp 5 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥](2nd𝑎) = 𝐽 ↔ (2nd𝑎) = 𝐽)
7168, 70anbi12i 629 . . . . . . . . . . . . . 14 (([(1st𝑎) / 𝑥]𝑥 = 𝐼[(1st𝑎) / 𝑥](2nd𝑎) = 𝐽) ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))
7263, 71bitri 278 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽) ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))
7362, 72anbi12i 629 . . . . . . . . . . . 12 (([(1st𝑎) / 𝑥]𝑧𝐷[(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
7459, 60, 733bitri 300 . . . . . . . . . . 11 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
7518, 43, 743bitr3g 316 . . . . . . . . . 10 (𝜑 → ((((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
7675anbi2d 631 . . . . . . . . 9 (𝜑 → ((𝑎 ∈ (V × V) ∧ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))))
7715, 76syl5bb 286 . . . . . . . 8 (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))))
78 xpss 5558 . . . . . . . . . . . 12 (𝑋 × 𝑌) ⊆ (V × V)
79 simprr 772 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
808adantrr 716 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8179, 80eqeltrd 2916 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
8278, 81sseldi 3951 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
8382ex 416 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
8483pm4.71rd 566 . . . . . . . . 9 (𝜑 → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩))))
85 eqop 7726 . . . . . . . . . . 11 (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
8685anbi2d 631 . . . . . . . . . 10 (𝑎 ∈ (V × V) → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
8786pm5.32i 578 . . . . . . . . 9 ((𝑎 ∈ (V × V) ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
8884, 87syl6rbb 291 . . . . . . . 8 (𝜑 → ((𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
8977, 88bitrd 282 . . . . . . 7 (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
9014, 89syl5bb 286 . . . . . 6 (𝜑 → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
9190opabbidv 5118 . . . . 5 (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)})
92 df-mpo 7154 . . . . . . . 8 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
933, 92eqtri 2847 . . . . . . 7 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
9493cnveqi 5732 . . . . . 6 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
95 nfv 1916 . . . . . . . 8 𝑖((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
96 nfv 1916 . . . . . . . 8 𝑗((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
97 nfv 1916 . . . . . . . . 9 𝑥(𝑖𝐴𝑗𝐵)
98 nfcsb1v 3890 . . . . . . . . . 10 𝑥𝑖 / 𝑥𝑗 / 𝑦𝐶
9998nfeq2 2999 . . . . . . . . 9 𝑥 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶
10097, 99nfan 1901 . . . . . . . 8 𝑥((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
101 nfv 1916 . . . . . . . . 9 𝑦(𝑖𝐴𝑗𝐵)
102 nfcv 2982 . . . . . . . . . . 11 𝑦𝑖
103 nfcsb1v 3890 . . . . . . . . . . 11 𝑦𝑗 / 𝑦𝐶
104102, 103nfcsbw 3892 . . . . . . . . . 10 𝑦𝑖 / 𝑥𝑗 / 𝑦𝐶
105104nfeq2 2999 . . . . . . . . 9 𝑦 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶
106101, 105nfan 1901 . . . . . . . 8 𝑦((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
107 simpl 486 . . . . . . . . . . 11 ((𝑥 = 𝑖𝑦 = 𝑗) → 𝑥 = 𝑖)
108107eleq1d 2900 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥𝐴𝑖𝐴))
109 simpr 488 . . . . . . . . . . 11 ((𝑥 = 𝑖𝑦 = 𝑗) → 𝑦 = 𝑗)
110109eleq1d 2900 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑦𝐵𝑗𝐵))
111108, 110anbi12d 633 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥𝐴𝑦𝐵) ↔ (𝑖𝐴𝑗𝐵)))
112 csbeq1a 3880 . . . . . . . . . . 11 (𝑦 = 𝑗𝐶 = 𝑗 / 𝑦𝐶)
113 csbeq1a 3880 . . . . . . . . . . 11 (𝑥 = 𝑖𝑗 / 𝑦𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
114112, 113sylan9eqr 2881 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → 𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
115114eqeq2d 2835 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑧 = 𝐶𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶))
116111, 115anbi12d 633 . . . . . . . 8 ((𝑥 = 𝑖𝑦 = 𝑗) → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)))
11795, 96, 100, 106, 116cbvoprab12 7236 . . . . . . 7 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)}
118117cnveqi 5732 . . . . . 6 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)}
119 eleq1 2903 . . . . . . . . 9 (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵)))
120 opelxp 5578 . . . . . . . . 9 (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖𝐴𝑗𝐵))
121119, 120syl6bb 290 . . . . . . . 8 (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑖𝐴𝑗𝐵)))
122 csbcom 4352 . . . . . . . . . . . . 13 (2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = 𝑖 / 𝑥(2nd𝑎) / 𝑗𝑗 / 𝑦𝐶
123 csbcow 3881 . . . . . . . . . . . . . 14 (2nd𝑎) / 𝑗𝑗 / 𝑦𝐶 = (2nd𝑎) / 𝑦𝐶
124123csbeq2i 3874 . . . . . . . . . . . . 13 𝑖 / 𝑥(2nd𝑎) / 𝑗𝑗 / 𝑦𝐶 = 𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶
125122, 124eqtri 2847 . . . . . . . . . . . 12 (2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = 𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶
126125csbeq2i 3874 . . . . . . . . . . 11 (1st𝑎) / 𝑖(2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = (1st𝑎) / 𝑖𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶
127 csbcow 3881 . . . . . . . . . . 11 (1st𝑎) / 𝑖𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
128126, 127eqtri 2847 . . . . . . . . . 10 (1st𝑎) / 𝑖(2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
129 csbopeq1a 7744 . . . . . . . . . 10 (𝑎 = ⟨𝑖, 𝑗⟩ → (1st𝑎) / 𝑖(2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
130128, 129syl5eqr 2873 . . . . . . . . 9 (𝑎 = ⟨𝑖, 𝑗⟩ → (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
131130eqeq2d 2835 . . . . . . . 8 (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶))
132121, 131anbi12d 633 . . . . . . 7 (𝑎 = ⟨𝑖, 𝑗⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)))
133 xpss 5558 . . . . . . . . 9 (𝐴 × 𝐵) ⊆ (V × V)
134133sseli 3949 . . . . . . . 8 (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
135134adantr 484 . . . . . . 7 ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) → 𝑎 ∈ (V × V))
136132, 135cnvoprab 7753 . . . . . 6 {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)}
13794, 118, 1363eqtri 2851 . . . . 5 𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)}
138 df-mpt 5133 . . . . 5 (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)}
13991, 137, 1383eqtr4g 2884 . . . 4 (𝜑𝐹 = (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩))
140139fneq1d 6434 . . 3 (𝜑 → (𝐹 Fn 𝐷 ↔ (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
14112, 140mpbird 260 . 2 (𝜑𝐹 Fn 𝐷)
142 dff1o4 6614 . 2 (𝐹:(𝐴 × 𝐵)–1-1-onto𝐷 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ 𝐹 Fn 𝐷))
1435, 141, 142sylanbrc 586 1 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wral 3133  Vcvv 3480  [wsbc 3758  csb 3866  cop 4556  {copab 5114  cmpt 5132   × cxp 5540  ccnv 5541   Fn wfn 6338  1-1-ontowf1o 6342  cfv 6343  {coprab 7150  cmpo 7151  1st c1st 7682  2nd c2nd 7683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-oprab 7153  df-mpo 7154  df-1st 7684  df-2nd 7685
This theorem is referenced by:  oddpwdc  31669
  Copyright terms: Public domain W3C validator