MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axcc2lem Structured version   Visualization version   GIF version

Theorem axcc2lem 10373
Description: Lemma for axcc2 10374. (Contributed by Mario Carneiro, 8-Feb-2013.)
Hypotheses
Ref Expression
axcc2lem.1 𝐾 = (𝑛 ∈ Ο‰ ↦ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)))
axcc2lem.2 𝐴 = (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›)))
axcc2lem.3 𝐺 = (𝑛 ∈ Ο‰ ↦ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
Assertion
Ref Expression
axcc2lem βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)))
Distinct variable groups:   𝐴,𝑓,𝑛   𝑓,𝐹,𝑔   𝑔,𝐺,𝑛   𝑛,𝐾
Allowed substitution hints:   𝐴(𝑔)   𝐹(𝑛)   𝐺(𝑓)   𝐾(𝑓,𝑔)

Proof of Theorem axcc2lem
Dummy variables π‘Ž 𝑧 π‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6856 . . . 4 (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ V
2 axcc2lem.3 . . . 4 𝐺 = (𝑛 ∈ Ο‰ ↦ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
31, 2fnmpti 6645 . . 3 𝐺 Fn Ο‰
4 vsnex 5387 . . . . . . . . . . . . . . 15 {𝑛} ∈ V
5 fvex 6856 . . . . . . . . . . . . . . 15 (πΎβ€˜π‘›) ∈ V
64, 5xpex 7688 . . . . . . . . . . . . . 14 ({𝑛} Γ— (πΎβ€˜π‘›)) ∈ V
7 axcc2lem.2 . . . . . . . . . . . . . . 15 𝐴 = (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›)))
87fvmpt2 6960 . . . . . . . . . . . . . 14 ((𝑛 ∈ Ο‰ ∧ ({𝑛} Γ— (πΎβ€˜π‘›)) ∈ V) β†’ (π΄β€˜π‘›) = ({𝑛} Γ— (πΎβ€˜π‘›)))
96, 8mpan2 690 . . . . . . . . . . . . 13 (𝑛 ∈ Ο‰ β†’ (π΄β€˜π‘›) = ({𝑛} Γ— (πΎβ€˜π‘›)))
10 vex 3450 . . . . . . . . . . . . . . 15 𝑛 ∈ V
1110snnz 4738 . . . . . . . . . . . . . 14 {𝑛} β‰  βˆ…
12 0ex 5265 . . . . . . . . . . . . . . . . . 18 βˆ… ∈ V
1312snnz 4738 . . . . . . . . . . . . . . . . 17 {βˆ…} β‰  βˆ…
14 iftrue 4493 . . . . . . . . . . . . . . . . . 18 ((πΉβ€˜π‘›) = βˆ… β†’ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) = {βˆ…})
1514neeq1d 3004 . . . . . . . . . . . . . . . . 17 ((πΉβ€˜π‘›) = βˆ… β†’ (if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) β‰  βˆ… ↔ {βˆ…} β‰  βˆ…))
1613, 15mpbiri 258 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘›) = βˆ… β†’ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) β‰  βˆ…)
17 iffalse 4496 . . . . . . . . . . . . . . . . 17 (Β¬ (πΉβ€˜π‘›) = βˆ… β†’ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) = (πΉβ€˜π‘›))
18 neqne 2952 . . . . . . . . . . . . . . . . 17 (Β¬ (πΉβ€˜π‘›) = βˆ… β†’ (πΉβ€˜π‘›) β‰  βˆ…)
1917, 18eqnetrd 3012 . . . . . . . . . . . . . . . 16 (Β¬ (πΉβ€˜π‘›) = βˆ… β†’ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) β‰  βˆ…)
2016, 19pm2.61i 182 . . . . . . . . . . . . . . 15 if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) β‰  βˆ…
21 p0ex 5340 . . . . . . . . . . . . . . . . . 18 {βˆ…} ∈ V
22 fvex 6856 . . . . . . . . . . . . . . . . . 18 (πΉβ€˜π‘›) ∈ V
2321, 22ifex 4537 . . . . . . . . . . . . . . . . 17 if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) ∈ V
24 axcc2lem.1 . . . . . . . . . . . . . . . . . 18 𝐾 = (𝑛 ∈ Ο‰ ↦ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)))
2524fvmpt2 6960 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ Ο‰ ∧ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) ∈ V) β†’ (πΎβ€˜π‘›) = if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)))
2623, 25mpan2 690 . . . . . . . . . . . . . . . 16 (𝑛 ∈ Ο‰ β†’ (πΎβ€˜π‘›) = if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)))
2726neeq1d 3004 . . . . . . . . . . . . . . 15 (𝑛 ∈ Ο‰ β†’ ((πΎβ€˜π‘›) β‰  βˆ… ↔ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) β‰  βˆ…))
2820, 27mpbiri 258 . . . . . . . . . . . . . 14 (𝑛 ∈ Ο‰ β†’ (πΎβ€˜π‘›) β‰  βˆ…)
29 xpnz 6112 . . . . . . . . . . . . . . 15 (({𝑛} β‰  βˆ… ∧ (πΎβ€˜π‘›) β‰  βˆ…) ↔ ({𝑛} Γ— (πΎβ€˜π‘›)) β‰  βˆ…)
3029biimpi 215 . . . . . . . . . . . . . 14 (({𝑛} β‰  βˆ… ∧ (πΎβ€˜π‘›) β‰  βˆ…) β†’ ({𝑛} Γ— (πΎβ€˜π‘›)) β‰  βˆ…)
3111, 28, 30sylancr 588 . . . . . . . . . . . . 13 (𝑛 ∈ Ο‰ β†’ ({𝑛} Γ— (πΎβ€˜π‘›)) β‰  βˆ…)
329, 31eqnetrd 3012 . . . . . . . . . . . 12 (𝑛 ∈ Ο‰ β†’ (π΄β€˜π‘›) β‰  βˆ…)
336, 7fnmpti 6645 . . . . . . . . . . . . . 14 𝐴 Fn Ο‰
34 fnfvelrn 7032 . . . . . . . . . . . . . 14 ((𝐴 Fn Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ (π΄β€˜π‘›) ∈ ran 𝐴)
3533, 34mpan 689 . . . . . . . . . . . . 13 (𝑛 ∈ Ο‰ β†’ (π΄β€˜π‘›) ∈ ran 𝐴)
36 neeq1 3007 . . . . . . . . . . . . . . 15 (𝑧 = (π΄β€˜π‘›) β†’ (𝑧 β‰  βˆ… ↔ (π΄β€˜π‘›) β‰  βˆ…))
37 fveq2 6843 . . . . . . . . . . . . . . . 16 (𝑧 = (π΄β€˜π‘›) β†’ (π‘“β€˜π‘§) = (π‘“β€˜(π΄β€˜π‘›)))
38 id 22 . . . . . . . . . . . . . . . 16 (𝑧 = (π΄β€˜π‘›) β†’ 𝑧 = (π΄β€˜π‘›))
3937, 38eleq12d 2832 . . . . . . . . . . . . . . 15 (𝑧 = (π΄β€˜π‘›) β†’ ((π‘“β€˜π‘§) ∈ 𝑧 ↔ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›)))
4036, 39imbi12d 345 . . . . . . . . . . . . . 14 (𝑧 = (π΄β€˜π‘›) β†’ ((𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ↔ ((π΄β€˜π‘›) β‰  βˆ… β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›))))
4140rspccv 3579 . . . . . . . . . . . . 13 (βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) β†’ ((π΄β€˜π‘›) ∈ ran 𝐴 β†’ ((π΄β€˜π‘›) β‰  βˆ… β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›))))
4235, 41syl5 34 . . . . . . . . . . . 12 (βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑛 ∈ Ο‰ β†’ ((π΄β€˜π‘›) β‰  βˆ… β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›))))
4332, 42mpdi 45 . . . . . . . . . . 11 (βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑛 ∈ Ο‰ β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›)))
4443impcom 409 . . . . . . . . . 10 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)) β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›))
459eleq2d 2824 . . . . . . . . . . 11 (𝑛 ∈ Ο‰ β†’ ((π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›) ↔ (π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΎβ€˜π‘›))))
4645adantr 482 . . . . . . . . . 10 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)) β†’ ((π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›) ↔ (π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΎβ€˜π‘›))))
4744, 46mpbid 231 . . . . . . . . 9 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)) β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΎβ€˜π‘›)))
48 xp2nd 7955 . . . . . . . . 9 ((π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΎβ€˜π‘›)) β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ (πΎβ€˜π‘›))
4947, 48syl 17 . . . . . . . 8 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)) β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ (πΎβ€˜π‘›))
50493adant3 1133 . . . . . . 7 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ∧ (πΉβ€˜π‘›) β‰  βˆ…) β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ (πΎβ€˜π‘›))
512fvmpt2 6960 . . . . . . . . . 10 ((𝑛 ∈ Ο‰ ∧ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ V) β†’ (πΊβ€˜π‘›) = (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
521, 51mpan2 690 . . . . . . . . 9 (𝑛 ∈ Ο‰ β†’ (πΊβ€˜π‘›) = (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
53523ad2ant1 1134 . . . . . . . 8 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ∧ (πΉβ€˜π‘›) β‰  βˆ…) β†’ (πΊβ€˜π‘›) = (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
5453eqcomd 2743 . . . . . . 7 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ∧ (πΉβ€˜π‘›) β‰  βˆ…) β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) = (πΊβ€˜π‘›))
55263ad2ant1 1134 . . . . . . . 8 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ∧ (πΉβ€˜π‘›) β‰  βˆ…) β†’ (πΎβ€˜π‘›) = if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)))
56 ifnefalse 4499 . . . . . . . . 9 ((πΉβ€˜π‘›) β‰  βˆ… β†’ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) = (πΉβ€˜π‘›))
57563ad2ant3 1136 . . . . . . . 8 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ∧ (πΉβ€˜π‘›) β‰  βˆ…) β†’ if((πΉβ€˜π‘›) = βˆ…, {βˆ…}, (πΉβ€˜π‘›)) = (πΉβ€˜π‘›))
5855, 57eqtrd 2777 . . . . . . 7 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ∧ (πΉβ€˜π‘›) β‰  βˆ…) β†’ (πΎβ€˜π‘›) = (πΉβ€˜π‘›))
5950, 54, 583eltr3d 2852 . . . . . 6 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ∧ (πΉβ€˜π‘›) β‰  βˆ…) β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))
60593expia 1122 . . . . 5 ((𝑛 ∈ Ο‰ ∧ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)) β†’ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)))
6160expcom 415 . . . 4 (βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑛 ∈ Ο‰ β†’ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))))
6261ralrimiv 3143 . . 3 (βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)))
63 omex 9580 . . . . 5 Ο‰ ∈ V
64 fnex 7168 . . . . 5 ((𝐺 Fn Ο‰ ∧ Ο‰ ∈ V) β†’ 𝐺 ∈ V)
653, 63, 64mp2an 691 . . . 4 𝐺 ∈ V
66 fneq1 6594 . . . . 5 (𝑔 = 𝐺 β†’ (𝑔 Fn Ο‰ ↔ 𝐺 Fn Ο‰))
67 fveq1 6842 . . . . . . . 8 (𝑔 = 𝐺 β†’ (π‘”β€˜π‘›) = (πΊβ€˜π‘›))
6867eleq1d 2823 . . . . . . 7 (𝑔 = 𝐺 β†’ ((π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ↔ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)))
6968imbi2d 341 . . . . . 6 (𝑔 = 𝐺 β†’ (((πΉβ€˜π‘›) β‰  βˆ… β†’ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ↔ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))))
7069ralbidv 3175 . . . . 5 (𝑔 = 𝐺 β†’ (βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ↔ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))))
7166, 70anbi12d 632 . . . 4 (𝑔 = 𝐺 β†’ ((𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) ↔ (𝐺 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)))))
7265, 71spcev 3566 . . 3 ((𝐺 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))) β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))))
733, 62, 72sylancr 588 . 2 (βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))))
746a1i 11 . . . . . 6 ((Ο‰ ∈ V ∧ 𝑛 ∈ Ο‰) β†’ ({𝑛} Γ— (πΎβ€˜π‘›)) ∈ V)
7574, 7fmptd 7063 . . . . 5 (Ο‰ ∈ V β†’ 𝐴:Ο‰βŸΆV)
7663, 75ax-mp 5 . . . 4 𝐴:Ο‰βŸΆV
77 sneq 4597 . . . . . . . . . 10 (𝑛 = π‘˜ β†’ {𝑛} = {π‘˜})
78 fveq2 6843 . . . . . . . . . 10 (𝑛 = π‘˜ β†’ (πΎβ€˜π‘›) = (πΎβ€˜π‘˜))
7977, 78xpeq12d 5665 . . . . . . . . 9 (𝑛 = π‘˜ β†’ ({𝑛} Γ— (πΎβ€˜π‘›)) = ({π‘˜} Γ— (πΎβ€˜π‘˜)))
8079, 7, 6fvmpt3i 6954 . . . . . . . 8 (π‘˜ ∈ Ο‰ β†’ (π΄β€˜π‘˜) = ({π‘˜} Γ— (πΎβ€˜π‘˜)))
8180adantl 483 . . . . . . 7 ((𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ (π΄β€˜π‘˜) = ({π‘˜} Γ— (πΎβ€˜π‘˜)))
8281eqeq2d 2748 . . . . . 6 ((𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) ↔ (π΄β€˜π‘›) = ({π‘˜} Γ— (πΎβ€˜π‘˜))))
839adantr 482 . . . . . . . 8 ((𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ (π΄β€˜π‘›) = ({𝑛} Γ— (πΎβ€˜π‘›)))
8483eqeq1d 2739 . . . . . . 7 ((𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ ((π΄β€˜π‘›) = ({π‘˜} Γ— (πΎβ€˜π‘˜)) ↔ ({𝑛} Γ— (πΎβ€˜π‘›)) = ({π‘˜} Γ— (πΎβ€˜π‘˜))))
85 xp11 6128 . . . . . . . . . 10 (({𝑛} β‰  βˆ… ∧ (πΎβ€˜π‘›) β‰  βˆ…) β†’ (({𝑛} Γ— (πΎβ€˜π‘›)) = ({π‘˜} Γ— (πΎβ€˜π‘˜)) ↔ ({𝑛} = {π‘˜} ∧ (πΎβ€˜π‘›) = (πΎβ€˜π‘˜))))
8611, 28, 85sylancr 588 . . . . . . . . 9 (𝑛 ∈ Ο‰ β†’ (({𝑛} Γ— (πΎβ€˜π‘›)) = ({π‘˜} Γ— (πΎβ€˜π‘˜)) ↔ ({𝑛} = {π‘˜} ∧ (πΎβ€˜π‘›) = (πΎβ€˜π‘˜))))
8710sneqr 4799 . . . . . . . . . 10 ({𝑛} = {π‘˜} β†’ 𝑛 = π‘˜)
8887adantr 482 . . . . . . . . 9 (({𝑛} = {π‘˜} ∧ (πΎβ€˜π‘›) = (πΎβ€˜π‘˜)) β†’ 𝑛 = π‘˜)
8986, 88syl6bi 253 . . . . . . . 8 (𝑛 ∈ Ο‰ β†’ (({𝑛} Γ— (πΎβ€˜π‘›)) = ({π‘˜} Γ— (πΎβ€˜π‘˜)) β†’ 𝑛 = π‘˜))
9089adantr 482 . . . . . . 7 ((𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ (({𝑛} Γ— (πΎβ€˜π‘›)) = ({π‘˜} Γ— (πΎβ€˜π‘˜)) β†’ 𝑛 = π‘˜))
9184, 90sylbid 239 . . . . . 6 ((𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ ((π΄β€˜π‘›) = ({π‘˜} Γ— (πΎβ€˜π‘˜)) β†’ 𝑛 = π‘˜))
9282, 91sylbid 239 . . . . 5 ((𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) β†’ 𝑛 = π‘˜))
9392rgen2 3195 . . . 4 βˆ€π‘› ∈ Ο‰ βˆ€π‘˜ ∈ Ο‰ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) β†’ 𝑛 = π‘˜)
94 dff13 7203 . . . 4 (𝐴:ω–1-1β†’V ↔ (𝐴:Ο‰βŸΆV ∧ βˆ€π‘› ∈ Ο‰ βˆ€π‘˜ ∈ Ο‰ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) β†’ 𝑛 = π‘˜)))
9576, 93, 94mpbir2an 710 . . 3 𝐴:ω–1-1β†’V
96 f1f1orn 6796 . . . 4 (𝐴:ω–1-1β†’V β†’ 𝐴:ω–1-1-ontoβ†’ran 𝐴)
9763f1oen 8914 . . . 4 (𝐴:ω–1-1-ontoβ†’ran 𝐴 β†’ Ο‰ β‰ˆ ran 𝐴)
98 ensym 8944 . . . 4 (Ο‰ β‰ˆ ran 𝐴 β†’ ran 𝐴 β‰ˆ Ο‰)
9996, 97, 983syl 18 . . 3 (𝐴:ω–1-1β†’V β†’ ran 𝐴 β‰ˆ Ο‰)
1007rneqi 5893 . . . . 5 ran 𝐴 = ran (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›)))
101 dmmptg 6195 . . . . . . . 8 (βˆ€π‘› ∈ Ο‰ ({𝑛} Γ— (πΎβ€˜π‘›)) ∈ V β†’ dom (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›))) = Ο‰)
1026a1i 11 . . . . . . . 8 (𝑛 ∈ Ο‰ β†’ ({𝑛} Γ— (πΎβ€˜π‘›)) ∈ V)
103101, 102mprg 3071 . . . . . . 7 dom (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›))) = Ο‰
104103, 63eqeltri 2834 . . . . . 6 dom (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›))) ∈ V
105 funmpt 6540 . . . . . 6 Fun (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›)))
106 funrnex 7887 . . . . . 6 (dom (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›))) ∈ V β†’ (Fun (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›))) β†’ ran (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›))) ∈ V))
107104, 105, 106mp2 9 . . . . 5 ran (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΎβ€˜π‘›))) ∈ V
108100, 107eqeltri 2834 . . . 4 ran 𝐴 ∈ V
109 breq1 5109 . . . . 5 (π‘Ž = ran 𝐴 β†’ (π‘Ž β‰ˆ Ο‰ ↔ ran 𝐴 β‰ˆ Ο‰))
110 raleq 3310 . . . . . 6 (π‘Ž = ran 𝐴 β†’ (βˆ€π‘§ ∈ π‘Ž (𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ↔ βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)))
111110exbidv 1925 . . . . 5 (π‘Ž = ran 𝐴 β†’ (βˆƒπ‘“βˆ€π‘§ ∈ π‘Ž (𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧) ↔ βˆƒπ‘“βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)))
112109, 111imbi12d 345 . . . 4 (π‘Ž = ran 𝐴 β†’ ((π‘Ž β‰ˆ Ο‰ β†’ βˆƒπ‘“βˆ€π‘§ ∈ π‘Ž (𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)) ↔ (ran 𝐴 β‰ˆ Ο‰ β†’ βˆƒπ‘“βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧))))
113 ax-cc 10372 . . . 4 (π‘Ž β‰ˆ Ο‰ β†’ βˆƒπ‘“βˆ€π‘§ ∈ π‘Ž (𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧))
114108, 112, 113vtocl 3519 . . 3 (ran 𝐴 β‰ˆ Ο‰ β†’ βˆƒπ‘“βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧))
11595, 99, 114mp2b 10 . 2 βˆƒπ‘“βˆ€π‘§ ∈ ran 𝐴(𝑧 β‰  βˆ… β†’ (π‘“β€˜π‘§) ∈ 𝑧)
11673, 115exlimiiv 1935 1 βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ ((πΉβ€˜π‘›) β‰  βˆ… β†’ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  Vcvv 3446  βˆ…c0 4283  ifcif 4487  {csn 4587   class class class wbr 5106   ↦ cmpt 5189   Γ— cxp 5632  dom cdm 5634  ran crn 5635  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€“1-1β†’wf1 6494  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  Ο‰com 7803  2nd c2nd 7921   β‰ˆ cen 8881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9578  ax-cc 10372
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-om 7804  df-2nd 7923  df-er 8649  df-en 8885
This theorem is referenced by:  axcc2  10374
  Copyright terms: Public domain W3C validator