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

Theorem xpmapenlem 6645
 Description: Lemma for xpmapen 6646. (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 6452 . . 3 𝑚 Fn (V × V)
2 xpmapen.1 . . . 4 𝐴 ∈ V
3 xpmapen.2 . . . 4 𝐵 ∈ V
42, 3xpex 4582 . . 3 (𝐴 × 𝐵) ∈ V
5 xpmapen.3 . . 3 𝐶 ∈ V
6 fnovex 5720 . . 3 (( ↑𝑚 Fn (V × V) ∧ (𝐴 × 𝐵) ∈ V ∧ 𝐶 ∈ V) → ((𝐴 × 𝐵) ↑𝑚 𝐶) ∈ V)
71, 4, 5, 6mp3an 1280 . 2 ((𝐴 × 𝐵) ↑𝑚 𝐶) ∈ V
8 fnovex 5720 . . . 4 (( ↑𝑚 Fn (V × V) ∧ 𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴𝑚 𝐶) ∈ V)
91, 2, 5, 8mp3an 1280 . . 3 (𝐴𝑚 𝐶) ∈ V
10 fnovex 5720 . . . 4 (( ↑𝑚 Fn (V × V) ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐵𝑚 𝐶) ∈ V)
111, 3, 5, 10mp3an 1280 . . 3 (𝐵𝑚 𝐶) ∈ V
129, 11xpex 4582 . 2 ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∈ V
134, 5elmap 6474 . . . . . . 7 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑥:𝐶⟶(𝐴 × 𝐵))
14 ffvelrn 5471 . . . . . . 7 ((𝑥:𝐶⟶(𝐴 × 𝐵) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
1513, 14sylanb 279 . . . . . 6 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
16 xp1st 5974 . . . . . 6 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (1st ‘(𝑥𝑧)) ∈ 𝐴)
1715, 16syl 14 . . . . 5 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) ∈ 𝐴)
18 xpmapenlem.4 . . . . 5 𝐷 = (𝑧𝐶 ↦ (1st ‘(𝑥𝑧)))
1917, 18fmptd 5491 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷:𝐶𝐴)
202, 5elmap 6474 . . . 4 (𝐷 ∈ (𝐴𝑚 𝐶) ↔ 𝐷:𝐶𝐴)
2119, 20sylibr 133 . . 3 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷 ∈ (𝐴𝑚 𝐶))
22 xp2nd 5975 . . . . . 6 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (2nd ‘(𝑥𝑧)) ∈ 𝐵)
2315, 22syl 14 . . . . 5 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) ∈ 𝐵)
24 xpmapenlem.5 . . . . 5 𝑅 = (𝑧𝐶 ↦ (2nd ‘(𝑥𝑧)))
2523, 24fmptd 5491 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅:𝐶𝐵)
263, 5elmap 6474 . . . 4 (𝑅 ∈ (𝐵𝑚 𝐶) ↔ 𝑅:𝐶𝐵)
2725, 26sylibr 133 . . 3 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅 ∈ (𝐵𝑚 𝐶))
28 opelxpi 4499 . . 3 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → ⟨𝐷, 𝑅⟩ ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)))
2921, 27, 28syl2anc 404 . 2 (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → ⟨𝐷, 𝑅⟩ ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)))
30 xp1st 5974 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦) ∈ (𝐴𝑚 𝐶))
312, 5elmap 6474 . . . . . . 7 ((1st𝑦) ∈ (𝐴𝑚 𝐶) ↔ (1st𝑦):𝐶𝐴)
3230, 31sylib 121 . . . . . 6 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦):𝐶𝐴)
3332ffvelrnda 5473 . . . . 5 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ((1st𝑦)‘𝑧) ∈ 𝐴)
34 xp2nd 5975 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦) ∈ (𝐵𝑚 𝐶))
353, 5elmap 6474 . . . . . . 7 ((2nd𝑦) ∈ (𝐵𝑚 𝐶) ↔ (2nd𝑦):𝐶𝐵)
3634, 35sylib 121 . . . . . 6 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦):𝐶𝐵)
3736ffvelrnda 5473 . . . . 5 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ((2nd𝑦)‘𝑧) ∈ 𝐵)
38 opelxpi 4499 . . . . 5 ((((1st𝑦)‘𝑧) ∈ 𝐴 ∧ ((2nd𝑦)‘𝑧) ∈ 𝐵) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ (𝐴 × 𝐵))
3933, 37, 38syl2anc 404 . . . 4 ((𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ (𝐴 × 𝐵))
40 xpmapenlem.6 . . . 4 𝑆 = (𝑧𝐶 ↦ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
4139, 40fmptd 5491 . . 3 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑆:𝐶⟶(𝐴 × 𝐵))
424, 5elmap 6474 . . 3 (𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑆:𝐶⟶(𝐴 × 𝐵))
4341, 42sylibr 133 . 2 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶))
44 1st2nd2 5983 . . . . 5 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
4544ad2antlr 474 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
4632feqmptd 5392 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (1st𝑦) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
4746ad2antlr 474 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st𝑦) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
48 simplr 498 . . . . . . . . . . . 12 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → 𝑥 = 𝑆)
4948fveq1d 5342 . . . . . . . . . . 11 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑥𝑧) = (𝑆𝑧))
50 vex 2636 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
51 1stexg 5976 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (1st𝑦) ∈ V)
5250, 51ax-mp 7 . . . . . . . . . . . . . . 15 (1st𝑦) ∈ V
53 vex 2636 . . . . . . . . . . . . . . 15 𝑧 ∈ V
5452, 53fvex 5360 . . . . . . . . . . . . . 14 ((1st𝑦)‘𝑧) ∈ V
55 2ndexg 5977 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (2nd𝑦) ∈ V)
5650, 55ax-mp 7 . . . . . . . . . . . . . . 15 (2nd𝑦) ∈ V
5756, 53fvex 5360 . . . . . . . . . . . . . 14 ((2nd𝑦)‘𝑧) ∈ V
5854, 57opex 4080 . . . . . . . . . . . . 13 ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ V
5940fvmpt2 5422 . . . . . . . . . . . . 13 ((𝑧𝐶 ∧ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ ∈ V) → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6058, 59mpan2 417 . . . . . . . . . . . 12 (𝑧𝐶 → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6160adantl 272 . . . . . . . . . . 11 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑆𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6249, 61eqtrd 2127 . . . . . . . . . 10 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (𝑥𝑧) = ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩)
6362fveq2d 5344 . . . . . . . . 9 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) = (1st ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩))
6454, 57op1st 5955 . . . . . . . . 9 (1st ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = ((1st𝑦)‘𝑧)
6563, 64syl6eq 2143 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (1st ‘(𝑥𝑧)) = ((1st𝑦)‘𝑧))
6665mpteq2dva 3950 . . . . . . 7 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧𝐶 ↦ (1st ‘(𝑥𝑧))) = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
6718, 66syl5eq 2139 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝐷 = (𝑧𝐶 ↦ ((1st𝑦)‘𝑧)))
6847, 67eqtr4d 2130 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st𝑦) = 𝐷)
6936feqmptd 5392 . . . . . . 7 (𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶)) → (2nd𝑦) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7069ad2antlr 474 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd𝑦) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7162fveq2d 5344 . . . . . . . . 9 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) = (2nd ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩))
7254, 57op2nd 5956 . . . . . . . . 9 (2nd ‘⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = ((2nd𝑦)‘𝑧)
7371, 72syl6eq 2143 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧𝐶) → (2nd ‘(𝑥𝑧)) = ((2nd𝑦)‘𝑧))
7473mpteq2dva 3950 . . . . . . 7 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧𝐶 ↦ (2nd ‘(𝑥𝑧))) = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7524, 74syl5eq 2139 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑅 = (𝑧𝐶 ↦ ((2nd𝑦)‘𝑧)))
7670, 75eqtr4d 2130 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd𝑦) = 𝑅)
7768, 76opeq12d 3652 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨𝐷, 𝑅⟩)
7845, 77eqtrd 2127 . . 3 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨𝐷, 𝑅⟩)
79 simpll 497 . . . . . 6 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶))
8079, 13sylib 121 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥:𝐶⟶(𝐴 × 𝐵))
8180feqmptd 5392 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = (𝑧𝐶 ↦ (𝑥𝑧)))
82 simpr 109 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑦 = ⟨𝐷, 𝑅⟩)
8382fveq2d 5344 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st𝑦) = (1st ‘⟨𝐷, 𝑅⟩))
8421ad2antrr 473 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝐷 ∈ (𝐴𝑚 𝐶))
8527ad2antrr 473 . . . . . . . . . . . 12 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑅 ∈ (𝐵𝑚 𝐶))
86 op1stg 5959 . . . . . . . . . . . 12 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → (1st ‘⟨𝐷, 𝑅⟩) = 𝐷)
8784, 85, 86syl2anc 404 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st ‘⟨𝐷, 𝑅⟩) = 𝐷)
8883, 87eqtrd 2127 . . . . . . . . . 10 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st𝑦) = 𝐷)
8988fveq1d 5342 . . . . . . . . 9 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((1st𝑦)‘𝑧) = (𝐷𝑧))
90 vex 2636 . . . . . . . . . . . 12 𝑥 ∈ V
9190, 53fvex 5360 . . . . . . . . . . 11 (𝑥𝑧) ∈ V
92 1stexg 5976 . . . . . . . . . . 11 ((𝑥𝑧) ∈ V → (1st ‘(𝑥𝑧)) ∈ V)
9391, 92ax-mp 7 . . . . . . . . . 10 (1st ‘(𝑥𝑧)) ∈ V
9418fvmpt2 5422 . . . . . . . . . 10 ((𝑧𝐶 ∧ (1st ‘(𝑥𝑧)) ∈ V) → (𝐷𝑧) = (1st ‘(𝑥𝑧)))
9593, 94mpan2 417 . . . . . . . . 9 (𝑧𝐶 → (𝐷𝑧) = (1st ‘(𝑥𝑧)))
9689, 95sylan9eq 2147 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ((1st𝑦)‘𝑧) = (1st ‘(𝑥𝑧)))
9782fveq2d 5344 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd𝑦) = (2nd ‘⟨𝐷, 𝑅⟩))
98 op2ndg 5960 . . . . . . . . . . . 12 ((𝐷 ∈ (𝐴𝑚 𝐶) ∧ 𝑅 ∈ (𝐵𝑚 𝐶)) → (2nd ‘⟨𝐷, 𝑅⟩) = 𝑅)
9984, 85, 98syl2anc 404 . . . . . . . . . . 11 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd ‘⟨𝐷, 𝑅⟩) = 𝑅)
10097, 99eqtrd 2127 . . . . . . . . . 10 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd𝑦) = 𝑅)
101100fveq1d 5342 . . . . . . . . 9 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((2nd𝑦)‘𝑧) = (𝑅𝑧))
102 2ndexg 5977 . . . . . . . . . . 11 ((𝑥𝑧) ∈ V → (2nd ‘(𝑥𝑧)) ∈ V)
10391, 102ax-mp 7 . . . . . . . . . 10 (2nd ‘(𝑥𝑧)) ∈ V
10424fvmpt2 5422 . . . . . . . . . 10 ((𝑧𝐶 ∧ (2nd ‘(𝑥𝑧)) ∈ V) → (𝑅𝑧) = (2nd ‘(𝑥𝑧)))
105103, 104mpan2 417 . . . . . . . . 9 (𝑧𝐶 → (𝑅𝑧) = (2nd ‘(𝑥𝑧)))
106101, 105sylan9eq 2147 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ((2nd𝑦)‘𝑧) = (2nd ‘(𝑥𝑧)))
10796, 106opeq12d 3652 . . . . . . 7 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
10880ffvelrnda 5473 . . . . . . . 8 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → (𝑥𝑧) ∈ (𝐴 × 𝐵))
109 1st2nd2 5983 . . . . . . . 8 ((𝑥𝑧) ∈ (𝐴 × 𝐵) → (𝑥𝑧) = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
110108, 109syl 14 . . . . . . 7 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → (𝑥𝑧) = ⟨(1st ‘(𝑥𝑧)), (2nd ‘(𝑥𝑧))⟩)
111107, 110eqtr4d 2130 . . . . . 6 ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧𝐶) → ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩ = (𝑥𝑧))
112111mpteq2dva 3950 . . . . 5 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (𝑧𝐶 ↦ ⟨((1st𝑦)‘𝑧), ((2nd𝑦)‘𝑧)⟩) = (𝑧𝐶 ↦ (𝑥𝑧)))
11340, 112syl5eq 2139 . . . 4 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑆 = (𝑧𝐶 ↦ (𝑥𝑧)))
11481, 113eqtr4d 2130 . . 3 (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = 𝑆)
11578, 114impbida 564 . 2 ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))) → (𝑥 = 𝑆𝑦 = ⟨𝐷, 𝑅⟩))
1167, 12, 29, 43, 115en3i 6568 1 ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴𝑚 𝐶) × (𝐵𝑚 𝐶))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   = wceq 1296   ∈ wcel 1445  Vcvv 2633  ⟨cop 3469   class class class wbr 3867   ↦ cmpt 3921   × cxp 4465   Fn wfn 5044  ⟶wf 5045  ‘cfv 5049  (class class class)co 5690  1st c1st 5947  2nd c2nd 5948   ↑𝑚 cmap 6445   ≈ cen 6535 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381 This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056  df-fv 5057  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-1st 5949  df-2nd 5950  df-map 6447  df-en 6538 This theorem is referenced by:  xpmapen  6646
 Copyright terms: Public domain W3C validator