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

Theorem xpmapenlem 6843
Description: Lemma for xpmapen 6844. (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 6649 . . 3 𝑚 Fn (V × V)
2 xpmapen.1 . . . 4 𝐴 ∈ V
3 xpmapen.2 . . . 4 𝐵 ∈ V
42, 3xpex 4738 . . 3 (𝐴 × 𝐵) ∈ V
5 xpmapen.3 . . 3 𝐶 ∈ V
6 fnovex 5902 . . 3 (( ↑𝑚 Fn (V × V) ∧ (𝐴 × 𝐵) ∈ V ∧ 𝐶 ∈ V) → ((𝐴 × 𝐵) ↑𝑚 𝐶) ∈ V)
71, 4, 5, 6mp3an 1337 . 2 ((𝐴 × 𝐵) ↑𝑚 𝐶) ∈ V
8 fnovex 5902 . . . 4 (( ↑𝑚 Fn (V × V) ∧ 𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴𝑚 𝐶) ∈ V)
91, 2, 5, 8mp3an 1337 . . 3 (𝐴𝑚 𝐶) ∈ V
10 fnovex 5902 . . . 4 (( ↑𝑚 Fn (V × V) ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐵𝑚 𝐶) ∈ V)
111, 3, 5, 10mp3an 1337 . . 3 (𝐵𝑚 𝐶) ∈ V
129, 11xpex 4738 . 2 ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∈ V
134, 5elmap 6671 . . . . . . 7 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑥:𝐶⟶(𝐴 × 𝐵))
14 ffvelcdm 5645 . . . . . . 7 ((𝑥:𝐶⟶(𝐴 × 𝐵) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
1513, 14sylanb 284 . . . . . 6 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
16 xp1st 6160 . . . . . 6 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (1st ‘(𝑥𝑧)) ∈ 𝐴)
1715, 16syl 14 . . . . 5 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) ∈ 𝐴)
18 xpmapenlem.4 . . . . 5 𝐷 = (𝑧𝐶 ↦ (1st ‘(𝑥𝑧)))
1917, 18fmptd 5666 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷:𝐶𝐴)
202, 5elmap 6671 . . . 4 (𝐷 ∈ (𝐴𝑚 𝐶) ↔ 𝐷:𝐶𝐴)
2119, 20sylibr 134 . . 3 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷 ∈ (𝐴𝑚 𝐶))
22 xp2nd 6161 . . . . . 6 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (2nd ‘(𝑥𝑧)) ∈ 𝐵)
2315, 22syl 14 . . . . 5 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) ∈ 𝐵)
24 xpmapenlem.5 . . . . 5 𝑅 = (𝑧𝐶 ↦ (2nd ‘(𝑥𝑧)))
2523, 24fmptd 5666 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅:𝐶𝐵)
263, 5elmap 6671 . . . 4 (𝑅 ∈ (𝐵𝑚 𝐶) ↔ 𝑅:𝐶𝐵)
2725, 26sylibr 134 . . 3 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅 ∈ (𝐵𝑚 𝐶))
28 opelxpi 4655 . . 3 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → ⟨𝐷, 𝑅⟩ ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)))
2921, 27, 28syl2anc 411 . 2 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → ⟨𝐷, 𝑅⟩ ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)))
30 xp1st 6160 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦) ∈ (𝐴𝑚 𝐶))
312, 5elmap 6671 . . . . . . 7 ((1st𝑦) ∈ (𝐴𝑚 𝐶) ↔ (1st𝑦):𝐶𝐴)
3230, 31sylib 122 . . . . . 6 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦):𝐶𝐴)
3332ffvelcdmda 5647 . . . . 5 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ((1st𝑦)‘𝑧) ∈ 𝐴)
34 xp2nd 6161 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦) ∈ (𝐵𝑚 𝐶))
353, 5elmap 6671 . . . . . . 7 ((2nd𝑦) ∈ (𝐵𝑚 𝐶) ↔ (2nd𝑦):𝐶𝐵)
3634, 35sylib 122 . . . . . 6 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦):𝐶𝐵)
3736ffvelcdmda 5647 . . . . 5 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ((2nd𝑦)‘𝑧) ∈ 𝐵)
38 opelxpi 4655 . . . . 5 ((((1st𝑦)‘𝑧) ∈ 𝐴 ∧ ((2nd𝑦)‘𝑧) ∈ 𝐵) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ (𝐴 × 𝐵))
3933, 37, 38syl2anc 411 . . . 4 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ (𝐴 × 𝐵))
40 xpmapenlem.6 . . . 4 𝑆 = (𝑧𝐶 ↦ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
4139, 40fmptd 5666 . . 3 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑆:𝐶⟶(𝐴 × 𝐵))
424, 5elmap 6671 . . 3 (𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑆:𝐶⟶(𝐴 × 𝐵))
4341, 42sylibr 134 . 2 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶))
44 1st2nd2 6170 . . . . 5 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
4544ad2antlr 489 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
4632feqmptd 5565 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
4746ad2antlr 489 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st𝑦) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
48 simplr 528 . . . . . . . . . . . 12 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → 𝑥 = 𝑆)
4948fveq1d 5513 . . . . . . . . . . 11 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑥𝑧) = (𝑆𝑧))
50 vex 2740 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
51 1stexg 6162 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (1st𝑦) ∈ V)
5250, 51ax-mp 5 . . . . . . . . . . . . . . 15 (1st𝑦) ∈ V
53 vex 2740 . . . . . . . . . . . . . . 15 𝑧 ∈ V
5452, 53fvex 5531 . . . . . . . . . . . . . 14 ((1st𝑦)‘𝑧) ∈ V
55 2ndexg 6163 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (2nd𝑦) ∈ V)
5650, 55ax-mp 5 . . . . . . . . . . . . . . 15 (2nd𝑦) ∈ V
5756, 53fvex 5531 . . . . . . . . . . . . . 14 ((2nd𝑦)‘𝑧) ∈ V
5854, 57opex 4226 . . . . . . . . . . . . 13 ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ V
5940fvmpt2 5595 . . . . . . . . . . . . 13 ((𝑧𝐶 ∧ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ V) → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6058, 59mpan2 425 . . . . . . . . . . . 12 (𝑧𝐶 → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6160adantl 277 . . . . . . . . . . 11 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6249, 61eqtrd 2210 . . . . . . . . . 10 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑥𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6362fveq2d 5515 . . . . . . . . 9 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) = (1st ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩))
6454, 57op1st 6141 . . . . . . . . 9 (1st ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = ((1st𝑦)‘𝑧)
6563, 64eqtrdi 2226 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) = ((1st𝑦)‘𝑧))
6665mpteq2dva 4090 . . . . . . 7 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧𝐶 ↦ (1st ‘(𝑥𝑧))) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
6718, 66eqtrid 2222 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝐷 = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
6847, 67eqtr4d 2213 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st𝑦) = 𝐷)
6936feqmptd 5565 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7069ad2antlr 489 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd𝑦) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7162fveq2d 5515 . . . . . . . . 9 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) = (2nd ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩))
7254, 57op2nd 6142 . . . . . . . . 9 (2nd ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = ((2nd𝑦)‘𝑧)
7371, 72eqtrdi 2226 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) = ((2nd𝑦)‘𝑧))
7473mpteq2dva 4090 . . . . . . 7 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧𝐶 ↦ (2nd ‘(𝑥𝑧))) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7524, 74eqtrid 2222 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑅 = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7670, 75eqtr4d 2213 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd𝑦) = 𝑅)
7768, 76opeq12d 3784 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨𝐷, 𝑅⟩)
7845, 77eqtrd 2210 . . 3 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨𝐷, 𝑅⟩)
79 simpll 527 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶))
8079, 13sylib 122 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥:𝐶⟶(𝐴 × 𝐵))
8180feqmptd 5565 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = (𝑧𝐶 ↦ (𝑥𝑧)))
82 simpr 110 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑦 = ⟨𝐷, 𝑅⟩)
8382fveq2d 5515 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st𝑦) = (1st ‘⟨𝐷, 𝑅⟩))
8421ad2antrr 488 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝐷 ∈ (𝐴𝑚 𝐶))
8527ad2antrr 488 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑅 ∈ (𝐵𝑚 𝐶))
86 op1stg 6145 . . . . . . . . . . . 12 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → (1st ‘⟨𝐷, 𝑅⟩) = 𝐷)
8784, 85, 86syl2anc 411 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st ‘⟨𝐷, 𝑅⟩) = 𝐷)
8883, 87eqtrd 2210 . . . . . . . . . 10 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st𝑦) = 𝐷)
8988fveq1d 5513 . . . . . . . . 9 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((1st𝑦)‘𝑧) = (𝐷𝑧))
90 vex 2740 . . . . . . . . . . . 12 𝑥 ∈ V
9190, 53fvex 5531 . . . . . . . . . . 11 (𝑥𝑧) ∈ V
92 1stexg 6162 . . . . . . . . . . 11 ((𝑥𝑧) ∈ V → (1st ‘(𝑥𝑧)) ∈ V)
9391, 92ax-mp 5 . . . . . . . . . 10 (1st ‘(𝑥𝑧)) ∈ V
9418fvmpt2 5595 . . . . . . . . . 10 ((𝑧𝐶 ∧ (1st ‘(𝑥𝑧)) ∈ V) → (𝐷𝑧) = (1st ‘(𝑥𝑧)))
9593, 94mpan2 425 . . . . . . . . 9 (𝑧𝐶 → (𝐷𝑧) = (1st ‘(𝑥𝑧)))
9689, 95sylan9eq 2230 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ((1st𝑦)‘𝑧) = (1st ‘(𝑥𝑧)))
9782fveq2d 5515 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd𝑦) = (2nd ‘⟨𝐷, 𝑅⟩))
98 op2ndg 6146 . . . . . . . . . . . 12 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → (2nd ‘⟨𝐷, 𝑅⟩) = 𝑅)
9984, 85, 98syl2anc 411 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd ‘⟨𝐷, 𝑅⟩) = 𝑅)
10097, 99eqtrd 2210 . . . . . . . . . 10 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd𝑦) = 𝑅)
101100fveq1d 5513 . . . . . . . . 9 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((2nd𝑦)‘𝑧) = (𝑅𝑧))
102 2ndexg 6163 . . . . . . . . . . 11 ((𝑥𝑧) ∈ V → (2nd ‘(𝑥𝑧)) ∈ V)
10391, 102ax-mp 5 . . . . . . . . . 10 (2nd ‘(𝑥𝑧)) ∈ V
10424fvmpt2 5595 . . . . . . . . . 10 ((𝑧𝐶 ∧ (2nd ‘(𝑥𝑧)) ∈ V) → (𝑅𝑧) = (2nd ‘(𝑥𝑧)))
105103, 104mpan2 425 . . . . . . . . 9 (𝑧𝐶 → (𝑅𝑧) = (2nd ‘(𝑥𝑧)))
106101, 105sylan9eq 2230 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ((2nd𝑦)‘𝑧) = (2nd ‘(𝑥𝑧)))
10796, 106opeq12d 3784 . . . . . . 7 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
10880ffvelcdmda 5647 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
109 1st2nd2 6170 . . . . . . . 8 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (𝑥𝑧) = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
110108, 109syl 14 . . . . . . 7 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → (𝑥𝑧) = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
111107, 110eqtr4d 2213 . . . . . 6 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ = (𝑥𝑧))
112111mpteq2dva 4090 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (𝑧𝐶 ↦ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = (𝑧𝐶 ↦ (𝑥𝑧)))
11340, 112eqtrid 2222 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑆 = (𝑧𝐶 ↦ (𝑥𝑧)))
11481, 113eqtr4d 2213 . . 3 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = 𝑆)
11578, 114impbida 596 . 2 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) → (𝑥 = 𝑆𝑦 = ⟨𝐷, 𝑅⟩))
1167, 12, 29, 43, 115en3i 6765 1 ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))
Colors of variables: wff set class
Syntax hints:  wa 104   = wceq 1353  wcel 2148  Vcvv 2737  cop 3594   class class class wbr 4000  cmpt 4061   × cxp 4621   Fn wfn 5207  wf 5208  cfv 5212  (class class class)co 5869  1st c1st 6133  2nd c2nd 6134  𝑚 cmap 6642  cen 6732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-map 6644  df-en 6735
This theorem is referenced by:  xpmapen  6844
  Copyright terms: Public domain W3C validator