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 30198
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 3135 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝐶𝑊)
3 f1od2.1 . . . 4 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
43fnmpo 7568 . . 3 (∀𝑥𝐴𝑦𝐵 𝐶𝑊𝐹 Fn (𝐴 × 𝐵))
52, 4syl 17 . 2 (𝜑𝐹 Fn (𝐴 × 𝐵))
6 f1od2.3 . . . . . 6 ((𝜑𝑧𝐷) → (𝐼𝑋𝐽𝑌))
7 opelxpi 5437 . . . . . 6 ((𝐼𝑋𝐽𝑌) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
86, 7syl 17 . . . . 5 ((𝜑𝑧𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
98ralrimiva 3126 . . . 4 (𝜑 → ∀𝑧𝐷𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
10 eqid 2772 . . . . 5 (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) = (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩)
1110fnmpt 6312 . . . 4 (∀𝑧𝐷𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌) → (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
129, 11syl 17 . . 3 (𝜑 → (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷)
13 elxp7 7529 . . . . . . . 8 (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)))
1413anbi1i 614 . . . . . . 7 ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ ((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
15 anass 461 . . . . . . . . 9 (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑎 ∈ (V × V) ∧ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)))
16 f1od2.4 . . . . . . . . . . . . 13 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
1716sbcbidv 3727 . . . . . . . . . . . 12 (𝜑 → ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
1817sbcbidv 3727 . . . . . . . . . . 11 (𝜑 → ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽))))
19 sbcan 3721 . . . . . . . . . . . . . 14 ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ∧ [(2nd𝑎) / 𝑦]𝑧 = 𝐶))
20 sbcan 3721 . . . . . . . . . . . . . . . 16 ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ↔ ([(2nd𝑎) / 𝑦]𝑥𝐴[(2nd𝑎) / 𝑦]𝑦𝐵))
21 fvex 6506 . . . . . . . . . . . . . . . . . 18 (2nd𝑎) ∈ V
22 sbcg 3746 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑥𝐴𝑥𝐴))
2321, 22ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑥𝐴𝑥𝐴)
24 sbcel1v 3738 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑦𝐵 ↔ (2nd𝑎) ∈ 𝐵)
2523, 24anbi12i 617 . . . . . . . . . . . . . . . 16 (([(2nd𝑎) / 𝑦]𝑥𝐴[(2nd𝑎) / 𝑦]𝑦𝐵) ↔ (𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵))
2620, 25bitri 267 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵))
27 sbceq2g 4248 . . . . . . . . . . . . . . . 16 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑎) / 𝑦𝐶))
2821, 27ax-mp 5 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑎) / 𝑦𝐶)
2926, 28anbi12i 617 . . . . . . . . . . . . . 14 (([(2nd𝑎) / 𝑦](𝑥𝐴𝑦𝐵) ∧ [(2nd𝑎) / 𝑦]𝑧 = 𝐶) ↔ ((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
3019, 29bitri 267 . . . . . . . . . . . . 13 ([(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
3130sbcbii 3728 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ [(1st𝑎) / 𝑥]((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶))
32 sbcan 3721 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥]((𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (2nd𝑎) / 𝑦𝐶) ↔ ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ [(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶))
33 sbcan 3721 . . . . . . . . . . . . . 14 ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ↔ ([(1st𝑎) / 𝑥]𝑥𝐴[(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵))
34 sbcel1v 3738 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥]𝑥𝐴 ↔ (1st𝑎) ∈ 𝐴)
35 fvex 6506 . . . . . . . . . . . . . . . 16 (1st𝑎) ∈ V
36 sbcg 3746 . . . . . . . . . . . . . . . 16 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵 ↔ (2nd𝑎) ∈ 𝐵))
3735, 36ax-mp 5 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵 ↔ (2nd𝑎) ∈ 𝐵)
3834, 37anbi12i 617 . . . . . . . . . . . . . 14 (([(1st𝑎) / 𝑥]𝑥𝐴[(1st𝑎) / 𝑥](2nd𝑎) ∈ 𝐵) ↔ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵))
3933, 38bitri 267 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ↔ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵))
40 sbceq2g 4248 . . . . . . . . . . . . . 14 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
4135, 40ax-mp 5 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)
4239, 41anbi12i 617 . . . . . . . . . . . 12 (([(1st𝑎) / 𝑥](𝑥𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ [(1st𝑎) / 𝑥]𝑧 = (2nd𝑎) / 𝑦𝐶) ↔ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
4331, 32, 423bitri 289 . . . . . . . . . . 11 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦]((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶))
44 sbcan 3721 . . . . . . . . . . . . . 14 ([(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ ([(2nd𝑎) / 𝑦]𝑧𝐷[(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽)))
45 sbcg 3746 . . . . . . . . . . . . . . . 16 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑧𝐷𝑧𝐷))
4621, 45ax-mp 5 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦]𝑧𝐷𝑧𝐷)
47 sbcan 3721 . . . . . . . . . . . . . . . 16 ([(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽) ↔ ([(2nd𝑎) / 𝑦]𝑥 = 𝐼[(2nd𝑎) / 𝑦]𝑦 = 𝐽))
48 sbcg 3746 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑥 = 𝐼𝑥 = 𝐼))
4921, 48ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑥 = 𝐼𝑥 = 𝐼)
50 sbceq1g 4246 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑎) ∈ V → ([(2nd𝑎) / 𝑦]𝑦 = 𝐽(2nd𝑎) / 𝑦𝑦 = 𝐽))
5121, 50ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([(2nd𝑎) / 𝑦]𝑦 = 𝐽(2nd𝑎) / 𝑦𝑦 = 𝐽)
5221csbvargi 4262 . . . . . . . . . . . . . . . . . . 19 (2nd𝑎) / 𝑦𝑦 = (2nd𝑎)
5352eqeq1i 2777 . . . . . . . . . . . . . . . . . 18 ((2nd𝑎) / 𝑦𝑦 = 𝐽 ↔ (2nd𝑎) = 𝐽)
5451, 53bitri 267 . . . . . . . . . . . . . . . . 17 ([(2nd𝑎) / 𝑦]𝑦 = 𝐽 ↔ (2nd𝑎) = 𝐽)
5549, 54anbi12i 617 . . . . . . . . . . . . . . . 16 (([(2nd𝑎) / 𝑦]𝑥 = 𝐼[(2nd𝑎) / 𝑦]𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽))
5647, 55bitri 267 . . . . . . . . . . . . . . 15 ([(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽) ↔ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽))
5746, 56anbi12i 617 . . . . . . . . . . . . . 14 (([(2nd𝑎) / 𝑦]𝑧𝐷[(2nd𝑎) / 𝑦](𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
5844, 57bitri 267 . . . . . . . . . . . . 13 ([(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
5958sbcbii 3728 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ [(1st𝑎) / 𝑥](𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
60 sbcan 3721 . . . . . . . . . . . 12 ([(1st𝑎) / 𝑥](𝑧𝐷 ∧ (𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)) ↔ ([(1st𝑎) / 𝑥]𝑧𝐷[(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)))
61 sbcg 3746 . . . . . . . . . . . . . 14 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑧𝐷𝑧𝐷))
6235, 61ax-mp 5 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥]𝑧𝐷𝑧𝐷)
63 sbcan 3721 . . . . . . . . . . . . . 14 ([(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽) ↔ ([(1st𝑎) / 𝑥]𝑥 = 𝐼[(1st𝑎) / 𝑥](2nd𝑎) = 𝐽))
64 sbceq1g 4246 . . . . . . . . . . . . . . . . 17 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥]𝑥 = 𝐼(1st𝑎) / 𝑥𝑥 = 𝐼))
6535, 64ax-mp 5 . . . . . . . . . . . . . . . 16 ([(1st𝑎) / 𝑥]𝑥 = 𝐼(1st𝑎) / 𝑥𝑥 = 𝐼)
6635csbvargi 4262 . . . . . . . . . . . . . . . . 17 (1st𝑎) / 𝑥𝑥 = (1st𝑎)
6766eqeq1i 2777 . . . . . . . . . . . . . . . 16 ((1st𝑎) / 𝑥𝑥 = 𝐼 ↔ (1st𝑎) = 𝐼)
6865, 67bitri 267 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥]𝑥 = 𝐼 ↔ (1st𝑎) = 𝐼)
69 sbcg 3746 . . . . . . . . . . . . . . . 16 ((1st𝑎) ∈ V → ([(1st𝑎) / 𝑥](2nd𝑎) = 𝐽 ↔ (2nd𝑎) = 𝐽))
7035, 69ax-mp 5 . . . . . . . . . . . . . . 15 ([(1st𝑎) / 𝑥](2nd𝑎) = 𝐽 ↔ (2nd𝑎) = 𝐽)
7168, 70anbi12i 617 . . . . . . . . . . . . . 14 (([(1st𝑎) / 𝑥]𝑥 = 𝐼[(1st𝑎) / 𝑥](2nd𝑎) = 𝐽) ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))
7263, 71bitri 267 . . . . . . . . . . . . 13 ([(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽) ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))
7362, 72anbi12i 617 . . . . . . . . . . . 12 (([(1st𝑎) / 𝑥]𝑧𝐷[(1st𝑎) / 𝑥](𝑥 = 𝐼 ∧ (2nd𝑎) = 𝐽)) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
7459, 60, 733bitri 289 . . . . . . . . . . 11 ([(1st𝑎) / 𝑥][(2nd𝑎) / 𝑦](𝑧𝐷 ∧ (𝑥 = 𝐼𝑦 = 𝐽)) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
7518, 43, 743bitr3g 305 . . . . . . . . . 10 (𝜑 → ((((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
7675anbi2d 619 . . . . . . . . 9 (𝜑 → ((𝑎 ∈ (V × V) ∧ (((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))))
7715, 76syl5bb 275 . . . . . . . 8 (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))))
78 xpss 5416 . . . . . . . . . . . 12 (𝑋 × 𝑌) ⊆ (V × V)
79 simprr 760 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 = ⟨𝐼, 𝐽⟩)
808adantrr 704 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → ⟨𝐼, 𝐽⟩ ∈ (𝑋 × 𝑌))
8179, 80eqeltrd 2860 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (𝑋 × 𝑌))
8278, 81sseldi 3852 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) → 𝑎 ∈ (V × V))
8382ex 405 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) → 𝑎 ∈ (V × V)))
8483pm4.71rd 555 . . . . . . . . 9 (𝜑 → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩))))
85 eqop 7536 . . . . . . . . . . 11 (𝑎 ∈ (V × V) → (𝑎 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽)))
8685anbi2d 619 . . . . . . . . . 10 (𝑎 ∈ (V × V) → ((𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩) ↔ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
8786pm5.32i 567 . . . . . . . . 9 ((𝑎 ∈ (V × V) ∧ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)) ↔ (𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))))
8884, 87syl6rbb 280 . . . . . . . 8 (𝜑 → ((𝑎 ∈ (V × V) ∧ (𝑧𝐷 ∧ ((1st𝑎) = 𝐼 ∧ (2nd𝑎) = 𝐽))) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
8977, 88bitrd 271 . . . . . . 7 (𝜑 → (((𝑎 ∈ (V × V) ∧ ((1st𝑎) ∈ 𝐴 ∧ (2nd𝑎) ∈ 𝐵)) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
9014, 89syl5bb 275 . . . . . 6 (𝜑 → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)))
9190opabbidv 4989 . . . . 5 (𝜑 → {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)})
92 df-mpo 6975 . . . . . . . 8 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
933, 92eqtri 2796 . . . . . . 7 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
9493cnveqi 5588 . . . . . 6 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
95 nfv 1873 . . . . . . . 8 𝑖((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
96 nfv 1873 . . . . . . . 8 𝑗((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
97 nfv 1873 . . . . . . . . 9 𝑥(𝑖𝐴𝑗𝐵)
98 nfcsb1v 3800 . . . . . . . . . 10 𝑥𝑖 / 𝑥𝑗 / 𝑦𝐶
9998nfeq2 2941 . . . . . . . . 9 𝑥 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶
10097, 99nfan 1862 . . . . . . . 8 𝑥((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
101 nfv 1873 . . . . . . . . 9 𝑦(𝑖𝐴𝑗𝐵)
102 nfcv 2926 . . . . . . . . . . 11 𝑦𝑖
103 nfcsb1v 3800 . . . . . . . . . . 11 𝑦𝑗 / 𝑦𝐶
104102, 103nfcsb 3802 . . . . . . . . . 10 𝑦𝑖 / 𝑥𝑗 / 𝑦𝐶
105104nfeq2 2941 . . . . . . . . 9 𝑦 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶
106101, 105nfan 1862 . . . . . . . 8 𝑦((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
107 simpl 475 . . . . . . . . . . 11 ((𝑥 = 𝑖𝑦 = 𝑗) → 𝑥 = 𝑖)
108107eleq1d 2844 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥𝐴𝑖𝐴))
109 simpr 477 . . . . . . . . . . 11 ((𝑥 = 𝑖𝑦 = 𝑗) → 𝑦 = 𝑗)
110109eleq1d 2844 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑦𝐵𝑗𝐵))
111108, 110anbi12d 621 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥𝐴𝑦𝐵) ↔ (𝑖𝐴𝑗𝐵)))
112 csbeq1a 3791 . . . . . . . . . . 11 (𝑦 = 𝑗𝐶 = 𝑗 / 𝑦𝐶)
113 csbeq1a 3791 . . . . . . . . . . 11 (𝑥 = 𝑖𝑗 / 𝑦𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
114112, 113sylan9eqr 2830 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → 𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
115114eqeq2d 2782 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑧 = 𝐶𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶))
116111, 115anbi12d 621 . . . . . . . 8 ((𝑥 = 𝑖𝑦 = 𝑗) → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)))
11795, 96, 100, 106, 116cbvoprab12 7053 . . . . . . 7 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)}
118117cnveqi 5588 . . . . . 6 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)}
119 eleq1 2847 . . . . . . . . 9 (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ ⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵)))
120 opelxp 5436 . . . . . . . . 9 (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖𝐴𝑗𝐵))
121119, 120syl6bb 279 . . . . . . . 8 (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑎 ∈ (𝐴 × 𝐵) ↔ (𝑖𝐴𝑗𝐵)))
122 csbcom 4252 . . . . . . . . . . . . 13 (2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = 𝑖 / 𝑥(2nd𝑎) / 𝑗𝑗 / 𝑦𝐶
123 csbco 3792 . . . . . . . . . . . . . 14 (2nd𝑎) / 𝑗𝑗 / 𝑦𝐶 = (2nd𝑎) / 𝑦𝐶
124123csbeq2i 4251 . . . . . . . . . . . . 13 𝑖 / 𝑥(2nd𝑎) / 𝑗𝑗 / 𝑦𝐶 = 𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶
125122, 124eqtri 2796 . . . . . . . . . . . 12 (2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = 𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶
126125csbeq2i 4251 . . . . . . . . . . 11 (1st𝑎) / 𝑖(2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = (1st𝑎) / 𝑖𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶
127 csbco 3792 . . . . . . . . . . 11 (1st𝑎) / 𝑖𝑖 / 𝑥(2nd𝑎) / 𝑦𝐶 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
128126, 127eqtri 2796 . . . . . . . . . 10 (1st𝑎) / 𝑖(2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶
129 csbopeq1a 7550 . . . . . . . . . 10 (𝑎 = ⟨𝑖, 𝑗⟩ → (1st𝑎) / 𝑖(2nd𝑎) / 𝑗𝑖 / 𝑥𝑗 / 𝑦𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
130128, 129syl5eqr 2822 . . . . . . . . 9 (𝑎 = ⟨𝑖, 𝑗⟩ → (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)
131130eqeq2d 2782 . . . . . . . 8 (𝑎 = ⟨𝑖, 𝑗⟩ → (𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶))
132121, 131anbi12d 621 . . . . . . 7 (𝑎 = ⟨𝑖, 𝑗⟩ → ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) ↔ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)))
133 xpss 5416 . . . . . . . . 9 (𝐴 × 𝐵) ⊆ (V × V)
134133sseli 3850 . . . . . . . 8 (𝑎 ∈ (𝐴 × 𝐵) → 𝑎 ∈ (V × V))
135134adantr 473 . . . . . . 7 ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶) → 𝑎 ∈ (V × V))
136132, 135cnvoprab 7559 . . . . . 6 {⟨⟨𝑖, 𝑗⟩, 𝑧⟩ ∣ ((𝑖𝐴𝑗𝐵) ∧ 𝑧 = 𝑖 / 𝑥𝑗 / 𝑦𝐶)} = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)}
13794, 118, 1363eqtri 2800 . . . . 5 𝐹 = {⟨𝑧, 𝑎⟩ ∣ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑧 = (1st𝑎) / 𝑥(2nd𝑎) / 𝑦𝐶)}
138 df-mpt 5003 . . . . 5 (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) = {⟨𝑧, 𝑎⟩ ∣ (𝑧𝐷𝑎 = ⟨𝐼, 𝐽⟩)}
13991, 137, 1383eqtr4g 2833 . . . 4 (𝜑𝐹 = (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩))
140139fneq1d 6273 . . 3 (𝜑 → (𝐹 Fn 𝐷 ↔ (𝑧𝐷 ↦ ⟨𝐼, 𝐽⟩) Fn 𝐷))
14112, 140mpbird 249 . 2 (𝜑𝐹 Fn 𝐷)
142 dff1o4 6446 . 2 (𝐹:(𝐴 × 𝐵)–1-1-onto𝐷 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ 𝐹 Fn 𝐷))
1435, 141, 142sylanbrc 575 1 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2048  wral 3082  Vcvv 3409  [wsbc 3677  csb 3782  cop 4441  {copab 4985  cmpt 5002   × cxp 5398  ccnv 5399   Fn wfn 6177  1-1-ontowf1o 6181  cfv 6182  {coprab 6971  cmpo 6972  1st c1st 7492  2nd c2nd 7493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-oprab 6974  df-mpo 6975  df-1st 7494  df-2nd 7495
This theorem is referenced by:  oddpwdc  31214
  Copyright terms: Public domain W3C validator