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

Theorem xpmapenlem 6519
Description: Lemma for xpmapen 6520. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
Hypotheses
Ref Expression
xpmapen.1 𝐴 ∈ V
xpmapen.2 𝐵 ∈ V
xpmapen.3 𝐶 ∈ V
xpmapenlem.4 𝐷 = (𝑧𝐶 ↦ (1st ‘(𝑥𝑧)))
xpmapenlem.5 𝑅 = (𝑧𝐶 ↦ (2nd ‘(𝑥𝑧)))
xpmapenlem.6 𝑆 = (𝑧𝐶 ↦ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
Assertion
Ref Expression
xpmapenlem ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑦,𝐷,𝑧   𝑦,𝑅,𝑧   𝑥,𝑆,𝑧
Allowed substitution hints:   𝐷(𝑥)   𝑅(𝑥)   𝑆(𝑦)

Proof of Theorem xpmapenlem
StepHypRef Expression
1 fnmap 6366 . . 3 𝑚 Fn (V × V)
2 xpmapen.1 . . . 4 𝐴 ∈ V
3 xpmapen.2 . . . 4 𝐵 ∈ V
42, 3xpex 4523 . . 3 (𝐴 × 𝐵) ∈ V
5 xpmapen.3 . . 3 𝐶 ∈ V
6 fnovex 5641 . . 3 (( ↑𝑚 Fn (V × V) ∧ (𝐴 × 𝐵) ∈ V ∧ 𝐶 ∈ V) → ((𝐴 × 𝐵) ↑𝑚 𝐶) ∈ V)
71, 4, 5, 6mp3an 1271 . 2 ((𝐴 × 𝐵) ↑𝑚 𝐶) ∈ V
8 fnovex 5641 . . . 4 (( ↑𝑚 Fn (V × V) ∧ 𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴𝑚 𝐶) ∈ V)
91, 2, 5, 8mp3an 1271 . . 3 (𝐴𝑚 𝐶) ∈ V
10 fnovex 5641 . . . 4 (( ↑𝑚 Fn (V × V) ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐵𝑚 𝐶) ∈ V)
111, 3, 5, 10mp3an 1271 . . 3 (𝐵𝑚 𝐶) ∈ V
129, 11xpex 4523 . 2 ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∈ V
134, 5elmap 6388 . . . . . . 7 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑥:𝐶⟶(𝐴 × 𝐵))
14 ffvelrn 5397 . . . . . . 7 ((𝑥:𝐶⟶(𝐴 × 𝐵) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
1513, 14sylanb 278 . . . . . 6 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
16 xp1st 5895 . . . . . 6 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (1st ‘(𝑥𝑧)) ∈ 𝐴)
1715, 16syl 14 . . . . 5 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) ∈ 𝐴)
18 xpmapenlem.4 . . . . 5 𝐷 = (𝑧𝐶 ↦ (1st ‘(𝑥𝑧)))
1917, 18fmptd 5417 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷:𝐶𝐴)
202, 5elmap 6388 . . . 4 (𝐷 ∈ (𝐴𝑚 𝐶) ↔ 𝐷:𝐶𝐴)
2119, 20sylibr 132 . . 3 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷 ∈ (𝐴𝑚 𝐶))
22 xp2nd 5896 . . . . . 6 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (2nd ‘(𝑥𝑧)) ∈ 𝐵)
2315, 22syl 14 . . . . 5 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) ∈ 𝐵)
24 xpmapenlem.5 . . . . 5 𝑅 = (𝑧𝐶 ↦ (2nd ‘(𝑥𝑧)))
2523, 24fmptd 5417 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅:𝐶𝐵)
263, 5elmap 6388 . . . 4 (𝑅 ∈ (𝐵𝑚 𝐶) ↔ 𝑅:𝐶𝐵)
2725, 26sylibr 132 . . 3 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅 ∈ (𝐵𝑚 𝐶))
28 opelxpi 4444 . . 3 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → ⟨𝐷, 𝑅⟩ ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)))
2921, 27, 28syl2anc 403 . 2 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → ⟨𝐷, 𝑅⟩ ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)))
30 xp1st 5895 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦) ∈ (𝐴𝑚 𝐶))
312, 5elmap 6388 . . . . . . 7 ((1st𝑦) ∈ (𝐴𝑚 𝐶) ↔ (1st𝑦):𝐶𝐴)
3230, 31sylib 120 . . . . . 6 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦):𝐶𝐴)
3332ffvelrnda 5399 . . . . 5 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ((1st𝑦)‘𝑧) ∈ 𝐴)
34 xp2nd 5896 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦) ∈ (𝐵𝑚 𝐶))
353, 5elmap 6388 . . . . . . 7 ((2nd𝑦) ∈ (𝐵𝑚 𝐶) ↔ (2nd𝑦):𝐶𝐵)
3634, 35sylib 120 . . . . . 6 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦):𝐶𝐵)
3736ffvelrnda 5399 . . . . 5 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ((2nd𝑦)‘𝑧) ∈ 𝐵)
38 opelxpi 4444 . . . . 5 ((((1st𝑦)‘𝑧) ∈ 𝐴 ∧ ((2nd𝑦)‘𝑧) ∈ 𝐵) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ (𝐴 × 𝐵))
3933, 37, 38syl2anc 403 . . . 4 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ (𝐴 × 𝐵))
40 xpmapenlem.6 . . . 4 𝑆 = (𝑧𝐶 ↦ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
4139, 40fmptd 5417 . . 3 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑆:𝐶⟶(𝐴 × 𝐵))
424, 5elmap 6388 . . 3 (𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑆:𝐶⟶(𝐴 × 𝐵))
4341, 42sylibr 132 . 2 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶))
44 1st2nd2 5904 . . . . 5 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
4544ad2antlr 473 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
4632feqmptd 5322 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
4746ad2antlr 473 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st𝑦) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
48 simplr 497 . . . . . . . . . . . 12 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → 𝑥 = 𝑆)
4948fveq1d 5272 . . . . . . . . . . 11 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑥𝑧) = (𝑆𝑧))
50 vex 2618 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
51 1stexg 5897 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (1st𝑦) ∈ V)
5250, 51ax-mp 7 . . . . . . . . . . . . . . 15 (1st𝑦) ∈ V
53 vex 2618 . . . . . . . . . . . . . . 15 𝑧 ∈ V
5452, 53fvex 5290 . . . . . . . . . . . . . 14 ((1st𝑦)‘𝑧) ∈ V
55 2ndexg 5898 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (2nd𝑦) ∈ V)
5650, 55ax-mp 7 . . . . . . . . . . . . . . 15 (2nd𝑦) ∈ V
5756, 53fvex 5290 . . . . . . . . . . . . . 14 ((2nd𝑦)‘𝑧) ∈ V
5854, 57opex 4032 . . . . . . . . . . . . 13 ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ V
5940fvmpt2 5351 . . . . . . . . . . . . 13 ((𝑧𝐶 ∧ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ V) → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6058, 59mpan2 416 . . . . . . . . . . . 12 (𝑧𝐶 → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6160adantl 271 . . . . . . . . . . 11 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6249, 61eqtrd 2117 . . . . . . . . . 10 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑥𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6362fveq2d 5274 . . . . . . . . 9 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) = (1st ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩))
6454, 57op1st 5876 . . . . . . . . 9 (1st ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = ((1st𝑦)‘𝑧)
6563, 64syl6eq 2133 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) = ((1st𝑦)‘𝑧))
6665mpteq2dva 3905 . . . . . . 7 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧𝐶 ↦ (1st ‘(𝑥𝑧))) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
6718, 66syl5eq 2129 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝐷 = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
6847, 67eqtr4d 2120 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st𝑦) = 𝐷)
6936feqmptd 5322 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7069ad2antlr 473 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd𝑦) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7162fveq2d 5274 . . . . . . . . 9 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) = (2nd ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩))
7254, 57op2nd 5877 . . . . . . . . 9 (2nd ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = ((2nd𝑦)‘𝑧)
7371, 72syl6eq 2133 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) = ((2nd𝑦)‘𝑧))
7473mpteq2dva 3905 . . . . . . 7 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧𝐶 ↦ (2nd ‘(𝑥𝑧))) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7524, 74syl5eq 2129 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑅 = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7670, 75eqtr4d 2120 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd𝑦) = 𝑅)
7768, 76opeq12d 3615 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨𝐷, 𝑅⟩)
7845, 77eqtrd 2117 . . 3 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨𝐷, 𝑅⟩)
79 simpll 496 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶))
8079, 13sylib 120 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥:𝐶⟶(𝐴 × 𝐵))
8180feqmptd 5322 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = (𝑧𝐶 ↦ (𝑥𝑧)))
82 simpr 108 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑦 = ⟨𝐷, 𝑅⟩)
8382fveq2d 5274 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st𝑦) = (1st ‘⟨𝐷, 𝑅⟩))
8421ad2antrr 472 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝐷 ∈ (𝐴𝑚 𝐶))
8527ad2antrr 472 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑅 ∈ (𝐵𝑚 𝐶))
86 op1stg 5880 . . . . . . . . . . . 12 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → (1st ‘⟨𝐷, 𝑅⟩) = 𝐷)
8784, 85, 86syl2anc 403 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st ‘⟨𝐷, 𝑅⟩) = 𝐷)
8883, 87eqtrd 2117 . . . . . . . . . 10 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st𝑦) = 𝐷)
8988fveq1d 5272 . . . . . . . . 9 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((1st𝑦)‘𝑧) = (𝐷𝑧))
90 vex 2618 . . . . . . . . . . . 12 𝑥 ∈ V
9190, 53fvex 5290 . . . . . . . . . . 11 (𝑥𝑧) ∈ V
92 1stexg 5897 . . . . . . . . . . 11 ((𝑥𝑧) ∈ V → (1st ‘(𝑥𝑧)) ∈ V)
9391, 92ax-mp 7 . . . . . . . . . 10 (1st ‘(𝑥𝑧)) ∈ V
9418fvmpt2 5351 . . . . . . . . . 10 ((𝑧𝐶 ∧ (1st ‘(𝑥𝑧)) ∈ V) → (𝐷𝑧) = (1st ‘(𝑥𝑧)))
9593, 94mpan2 416 . . . . . . . . 9 (𝑧𝐶 → (𝐷𝑧) = (1st ‘(𝑥𝑧)))
9689, 95sylan9eq 2137 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ((1st𝑦)‘𝑧) = (1st ‘(𝑥𝑧)))
9782fveq2d 5274 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd𝑦) = (2nd ‘⟨𝐷, 𝑅⟩))
98 op2ndg 5881 . . . . . . . . . . . 12 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → (2nd ‘⟨𝐷, 𝑅⟩) = 𝑅)
9984, 85, 98syl2anc 403 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd ‘⟨𝐷, 𝑅⟩) = 𝑅)
10097, 99eqtrd 2117 . . . . . . . . . 10 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd𝑦) = 𝑅)
101100fveq1d 5272 . . . . . . . . 9 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((2nd𝑦)‘𝑧) = (𝑅𝑧))
102 2ndexg 5898 . . . . . . . . . . 11 ((𝑥𝑧) ∈ V → (2nd ‘(𝑥𝑧)) ∈ V)
10391, 102ax-mp 7 . . . . . . . . . 10 (2nd ‘(𝑥𝑧)) ∈ V
10424fvmpt2 5351 . . . . . . . . . 10 ((𝑧𝐶 ∧ (2nd ‘(𝑥𝑧)) ∈ V) → (𝑅𝑧) = (2nd ‘(𝑥𝑧)))
105103, 104mpan2 416 . . . . . . . . 9 (𝑧𝐶 → (𝑅𝑧) = (2nd ‘(𝑥𝑧)))
106101, 105sylan9eq 2137 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ((2nd𝑦)‘𝑧) = (2nd ‘(𝑥𝑧)))
10796, 106opeq12d 3615 . . . . . . 7 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
10880ffvelrnda 5399 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
109 1st2nd2 5904 . . . . . . . 8 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (𝑥𝑧) = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
110108, 109syl 14 . . . . . . 7 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → (𝑥𝑧) = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
111107, 110eqtr4d 2120 . . . . . 6 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ = (𝑥𝑧))
112111mpteq2dva 3905 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (𝑧𝐶 ↦ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = (𝑧𝐶 ↦ (𝑥𝑧)))
11340, 112syl5eq 2129 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑆 = (𝑧𝐶 ↦ (𝑥𝑧)))
11481, 113eqtr4d 2120 . . 3 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = 𝑆)
11578, 114impbida 561 . 2 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) → (𝑥 = 𝑆𝑦 = ⟨𝐷, 𝑅⟩))
1167, 12, 29, 43, 115en3i 6442 1 ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))
Colors of variables: wff set class
Syntax hints:  wa 102   = wceq 1287  wcel 1436  Vcvv 2615  cop 3434   class class class wbr 3822  cmpt 3876   × cxp 4411   Fn wfn 4978  wf 4979  cfv 4983  (class class class)co 5615  1st c1st 5868  2nd c2nd 5869  𝑚 cmap 6359  cen 6409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-id 4096  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-1st 5870  df-2nd 5871  df-map 6361  df-en 6412
This theorem is referenced by:  xpmapen  6520
  Copyright terms: Public domain W3C validator