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

Theorem cnfcom3lem 9700
Description: Lemma for cnfcom3 9701. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 4-Jul-2019.)
Hypotheses
Ref Expression
cnfcom.s ๐‘† = dom (ฯ‰ CNF ๐ด)
cnfcom.a (๐œ‘ โ†’ ๐ด โˆˆ On)
cnfcom.b (๐œ‘ โ†’ ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด))
cnfcom.f ๐น = (โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต)
cnfcom.g ๐บ = OrdIso( E , (๐น supp โˆ…))
cnfcom.h ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (๐‘€ +o ๐‘ง)), โˆ…)
cnfcom.t ๐‘‡ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘“ โˆˆ V โ†ฆ ๐พ), โˆ…)
cnfcom.m ๐‘€ = ((ฯ‰ โ†‘o (๐บโ€˜๐‘˜)) ยทo (๐นโ€˜(๐บโ€˜๐‘˜)))
cnfcom.k ๐พ = ((๐‘ฅ โˆˆ ๐‘€ โ†ฆ (dom ๐‘“ +o ๐‘ฅ)) โˆช โ—ก(๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ (๐‘€ +o ๐‘ฅ)))
cnfcom.w ๐‘Š = (๐บโ€˜โˆช dom ๐บ)
cnfcom3.1 (๐œ‘ โ†’ ฯ‰ โІ ๐ต)
Assertion
Ref Expression
cnfcom3lem (๐œ‘ โ†’ ๐‘Š โˆˆ (On โˆ– 1o))
Distinct variable groups:   ๐‘ฅ,๐‘˜,๐‘ง,๐ด   ๐‘ฅ,๐‘€   ๐‘“,๐‘˜,๐‘ฅ,๐‘ง,๐น   ๐‘ง,๐‘‡   ๐‘ฅ,๐‘Š   ๐‘“,๐บ,๐‘˜,๐‘ฅ,๐‘ง   ๐‘“,๐ป,๐‘ฅ   ๐‘†,๐‘˜,๐‘ง   ๐œ‘,๐‘˜,๐‘ฅ,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘“)   ๐ด(๐‘“)   ๐ต(๐‘ฅ,๐‘ง,๐‘“,๐‘˜)   ๐‘†(๐‘ฅ,๐‘“)   ๐‘‡(๐‘ฅ,๐‘“,๐‘˜)   ๐ป(๐‘ง,๐‘˜)   ๐พ(๐‘ฅ,๐‘ง,๐‘“,๐‘˜)   ๐‘€(๐‘ง,๐‘“,๐‘˜)   ๐‘Š(๐‘ง,๐‘“,๐‘˜)

Proof of Theorem cnfcom3lem
StepHypRef Expression
1 cnfcom.w . . 3 ๐‘Š = (๐บโ€˜โˆช dom ๐บ)
2 cnfcom.a . . . 4 (๐œ‘ โ†’ ๐ด โˆˆ On)
3 suppssdm 8162 . . . . . 6 (๐น supp โˆ…) โІ dom ๐น
4 cnfcom.f . . . . . . . . 9 ๐น = (โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต)
5 cnfcom.s . . . . . . . . . . . 12 ๐‘† = dom (ฯ‰ CNF ๐ด)
6 omelon 9643 . . . . . . . . . . . . 13 ฯ‰ โˆˆ On
76a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ ฯ‰ โˆˆ On)
85, 7, 2cantnff1o 9693 . . . . . . . . . . 11 (๐œ‘ โ†’ (ฯ‰ CNF ๐ด):๐‘†โ€“1-1-ontoโ†’(ฯ‰ โ†‘o ๐ด))
9 f1ocnv 6839 . . . . . . . . . . 11 ((ฯ‰ CNF ๐ด):๐‘†โ€“1-1-ontoโ†’(ฯ‰ โ†‘o ๐ด) โ†’ โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โ€“1-1-ontoโ†’๐‘†)
10 f1of 6827 . . . . . . . . . . 11 (โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โ€“1-1-ontoโ†’๐‘† โ†’ โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โŸถ๐‘†)
118, 9, 103syl 18 . . . . . . . . . 10 (๐œ‘ โ†’ โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โŸถ๐‘†)
12 cnfcom.b . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด))
1311, 12ffvelcdmd 7081 . . . . . . . . 9 (๐œ‘ โ†’ (โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต) โˆˆ ๐‘†)
144, 13eqeltrid 2831 . . . . . . . 8 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
155, 7, 2cantnfs 9663 . . . . . . . 8 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โ†” (๐น:๐ดโŸถฯ‰ โˆง ๐น finSupp โˆ…)))
1614, 15mpbid 231 . . . . . . 7 (๐œ‘ โ†’ (๐น:๐ดโŸถฯ‰ โˆง ๐น finSupp โˆ…))
1716simpld 494 . . . . . 6 (๐œ‘ โ†’ ๐น:๐ดโŸถฯ‰)
183, 17fssdm 6731 . . . . 5 (๐œ‘ โ†’ (๐น supp โˆ…) โІ ๐ด)
19 ovex 7438 . . . . . . . . . . 11 (๐น supp โˆ…) โˆˆ V
20 cnfcom.g . . . . . . . . . . . 12 ๐บ = OrdIso( E , (๐น supp โˆ…))
2120oion 9533 . . . . . . . . . . 11 ((๐น supp โˆ…) โˆˆ V โ†’ dom ๐บ โˆˆ On)
2219, 21ax-mp 5 . . . . . . . . . 10 dom ๐บ โˆˆ On
2322elexi 3488 . . . . . . . . 9 dom ๐บ โˆˆ V
2423uniex 7728 . . . . . . . 8 โˆช dom ๐บ โˆˆ V
2524sucid 6440 . . . . . . 7 โˆช dom ๐บ โˆˆ suc โˆช dom ๐บ
26 cnfcom.h . . . . . . . 8 ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (๐‘€ +o ๐‘ง)), โˆ…)
27 cnfcom.t . . . . . . . 8 ๐‘‡ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘“ โˆˆ V โ†ฆ ๐พ), โˆ…)
28 cnfcom.m . . . . . . . 8 ๐‘€ = ((ฯ‰ โ†‘o (๐บโ€˜๐‘˜)) ยทo (๐นโ€˜(๐บโ€˜๐‘˜)))
29 cnfcom.k . . . . . . . 8 ๐พ = ((๐‘ฅ โˆˆ ๐‘€ โ†ฆ (dom ๐‘“ +o ๐‘ฅ)) โˆช โ—ก(๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ (๐‘€ +o ๐‘ฅ)))
30 cnfcom3.1 . . . . . . . . 9 (๐œ‘ โ†’ ฯ‰ โІ ๐ต)
31 peano1 7876 . . . . . . . . . 10 โˆ… โˆˆ ฯ‰
3231a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ โˆ… โˆˆ ฯ‰)
3330, 32sseldd 3978 . . . . . . . 8 (๐œ‘ โ†’ โˆ… โˆˆ ๐ต)
345, 2, 12, 4, 20, 26, 27, 28, 29, 1, 33cnfcom2lem 9698 . . . . . . 7 (๐œ‘ โ†’ dom ๐บ = suc โˆช dom ๐บ)
3525, 34eleqtrrid 2834 . . . . . 6 (๐œ‘ โ†’ โˆช dom ๐บ โˆˆ dom ๐บ)
3620oif 9527 . . . . . . 7 ๐บ:dom ๐บโŸถ(๐น supp โˆ…)
3736ffvelcdmi 7079 . . . . . 6 (โˆช dom ๐บ โˆˆ dom ๐บ โ†’ (๐บโ€˜โˆช dom ๐บ) โˆˆ (๐น supp โˆ…))
3835, 37syl 17 . . . . 5 (๐œ‘ โ†’ (๐บโ€˜โˆช dom ๐บ) โˆˆ (๐น supp โˆ…))
3918, 38sseldd 3978 . . . 4 (๐œ‘ โ†’ (๐บโ€˜โˆช dom ๐บ) โˆˆ ๐ด)
40 onelon 6383 . . . 4 ((๐ด โˆˆ On โˆง (๐บโ€˜โˆช dom ๐บ) โˆˆ ๐ด) โ†’ (๐บโ€˜โˆช dom ๐บ) โˆˆ On)
412, 39, 40syl2anc 583 . . 3 (๐œ‘ โ†’ (๐บโ€˜โˆช dom ๐บ) โˆˆ On)
421, 41eqeltrid 2831 . 2 (๐œ‘ โ†’ ๐‘Š โˆˆ On)
43 oecl 8538 . . . . . . 7 ((ฯ‰ โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (ฯ‰ โ†‘o ๐ด) โˆˆ On)
446, 2, 43sylancr 586 . . . . . 6 (๐œ‘ โ†’ (ฯ‰ โ†‘o ๐ด) โˆˆ On)
45 onelon 6383 . . . . . 6 (((ฯ‰ โ†‘o ๐ด) โˆˆ On โˆง ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด)) โ†’ ๐ต โˆˆ On)
4644, 12, 45syl2anc 583 . . . . 5 (๐œ‘ โ†’ ๐ต โˆˆ On)
47 ontri1 6392 . . . . 5 ((ฯ‰ โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (ฯ‰ โІ ๐ต โ†” ยฌ ๐ต โˆˆ ฯ‰))
486, 46, 47sylancr 586 . . . 4 (๐œ‘ โ†’ (ฯ‰ โІ ๐ต โ†” ยฌ ๐ต โˆˆ ฯ‰))
4930, 48mpbid 231 . . 3 (๐œ‘ โ†’ ยฌ ๐ต โˆˆ ฯ‰)
504fveq2i 6888 . . . . . . . 8 ((ฯ‰ CNF ๐ด)โ€˜๐น) = ((ฯ‰ CNF ๐ด)โ€˜(โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต))
51 f1ocnvfv2 7271 . . . . . . . . 9 (((ฯ‰ CNF ๐ด):๐‘†โ€“1-1-ontoโ†’(ฯ‰ โ†‘o ๐ด) โˆง ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด)) โ†’ ((ฯ‰ CNF ๐ด)โ€˜(โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต)) = ๐ต)
528, 12, 51syl2anc 583 . . . . . . . 8 (๐œ‘ โ†’ ((ฯ‰ CNF ๐ด)โ€˜(โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต)) = ๐ต)
5350, 52eqtrid 2778 . . . . . . 7 (๐œ‘ โ†’ ((ฯ‰ CNF ๐ด)โ€˜๐น) = ๐ต)
5453adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ ((ฯ‰ CNF ๐ด)โ€˜๐น) = ๐ต)
556a1i 11 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ ฯ‰ โˆˆ On)
562adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ ๐ด โˆˆ On)
5714adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ ๐น โˆˆ ๐‘†)
5831a1i 11 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ โˆ… โˆˆ ฯ‰)
59 1on 8479 . . . . . . . . 9 1o โˆˆ On
6059a1i 11 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ 1o โˆˆ On)
61 ovexd 7440 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐น supp โˆ…) โˆˆ V)
625, 7, 2, 20, 14cantnfcl 9664 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ( E We (๐น supp โˆ…) โˆง dom ๐บ โˆˆ ฯ‰))
6362simpld 494 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ E We (๐น supp โˆ…))
6420oiiso 9534 . . . . . . . . . . . . . . . . . . . 20 (((๐น supp โˆ…) โˆˆ V โˆง E We (๐น supp โˆ…)) โ†’ ๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)))
6561, 63, 64syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)))
6665ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)))
67 isof1o 7316 . . . . . . . . . . . . . . . . . 18 (๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)) โ†’ ๐บ:dom ๐บโ€“1-1-ontoโ†’(๐น supp โˆ…))
6866, 67syl 17 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ๐บ:dom ๐บโ€“1-1-ontoโ†’(๐น supp โˆ…))
69 f1ocnv 6839 . . . . . . . . . . . . . . . . 17 (๐บ:dom ๐บโ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ โ—ก๐บ:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐บ)
70 f1of 6827 . . . . . . . . . . . . . . . . 17 (โ—ก๐บ:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐บ โ†’ โ—ก๐บ:(๐น supp โˆ…)โŸถdom ๐บ)
7168, 69, 703syl 18 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ โ—ก๐บ:(๐น supp โˆ…)โŸถdom ๐บ)
72 ffvelcdm 7077 . . . . . . . . . . . . . . . 16 ((โ—ก๐บ:(๐น supp โˆ…)โŸถdom ๐บ โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (โ—ก๐บโ€˜๐‘ฅ) โˆˆ dom ๐บ)
7371, 72sylancom 587 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (โ—ก๐บโ€˜๐‘ฅ) โˆˆ dom ๐บ)
74 elssuni 4934 . . . . . . . . . . . . . . 15 ((โ—ก๐บโ€˜๐‘ฅ) โˆˆ dom ๐บ โ†’ (โ—ก๐บโ€˜๐‘ฅ) โІ โˆช dom ๐บ)
7573, 74syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (โ—ก๐บโ€˜๐‘ฅ) โІ โˆช dom ๐บ)
76 onelon 6383 . . . . . . . . . . . . . . . 16 ((dom ๐บ โˆˆ On โˆง (โ—ก๐บโ€˜๐‘ฅ) โˆˆ dom ๐บ) โ†’ (โ—ก๐บโ€˜๐‘ฅ) โˆˆ On)
7722, 73, 76sylancr 586 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (โ—ก๐บโ€˜๐‘ฅ) โˆˆ On)
78 onuni 7773 . . . . . . . . . . . . . . . 16 (dom ๐บ โˆˆ On โ†’ โˆช dom ๐บ โˆˆ On)
7922, 78ax-mp 5 . . . . . . . . . . . . . . 15 โˆช dom ๐บ โˆˆ On
80 ontri1 6392 . . . . . . . . . . . . . . 15 (((โ—ก๐บโ€˜๐‘ฅ) โˆˆ On โˆง โˆช dom ๐บ โˆˆ On) โ†’ ((โ—ก๐บโ€˜๐‘ฅ) โІ โˆช dom ๐บ โ†” ยฌ โˆช dom ๐บ โˆˆ (โ—ก๐บโ€˜๐‘ฅ)))
8177, 79, 80sylancl 585 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ((โ—ก๐บโ€˜๐‘ฅ) โІ โˆช dom ๐บ โ†” ยฌ โˆช dom ๐บ โˆˆ (โ—ก๐บโ€˜๐‘ฅ)))
8275, 81mpbid 231 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ยฌ โˆช dom ๐บ โˆˆ (โ—ก๐บโ€˜๐‘ฅ))
8335ad2antrr 723 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ โˆช dom ๐บ โˆˆ dom ๐บ)
84 isorel 7319 . . . . . . . . . . . . . . . 16 ((๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)) โˆง (โˆช dom ๐บ โˆˆ dom ๐บ โˆง (โ—ก๐บโ€˜๐‘ฅ) โˆˆ dom ๐บ)) โ†’ (โˆช dom ๐บ E (โ—ก๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜โˆช dom ๐บ) E (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ))))
8566, 83, 73, 84syl12anc 834 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (โˆช dom ๐บ E (โ—ก๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜โˆช dom ๐บ) E (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ))))
86 fvex 6898 . . . . . . . . . . . . . . . 16 (โ—ก๐บโ€˜๐‘ฅ) โˆˆ V
8786epeli 5575 . . . . . . . . . . . . . . 15 (โˆช dom ๐บ E (โ—ก๐บโ€˜๐‘ฅ) โ†” โˆช dom ๐บ โˆˆ (โ—ก๐บโ€˜๐‘ฅ))
881breq1i 5148 . . . . . . . . . . . . . . . 16 (๐‘Š E (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)) โ†” (๐บโ€˜โˆช dom ๐บ) E (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)))
89 fvex 6898 . . . . . . . . . . . . . . . . 17 (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)) โˆˆ V
9089epeli 5575 . . . . . . . . . . . . . . . 16 (๐‘Š E (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)) โ†” ๐‘Š โˆˆ (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)))
9188, 90bitr3i 277 . . . . . . . . . . . . . . 15 ((๐บโ€˜โˆช dom ๐บ) E (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)) โ†” ๐‘Š โˆˆ (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)))
9285, 87, 913bitr3g 313 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (โˆช dom ๐บ โˆˆ (โ—ก๐บโ€˜๐‘ฅ) โ†” ๐‘Š โˆˆ (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ))))
93 simplr 766 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ๐‘Š = โˆ…)
94 f1ocnvfv2 7271 . . . . . . . . . . . . . . . 16 ((๐บ:dom ๐บโ€“1-1-ontoโ†’(๐น supp โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)) = ๐‘ฅ)
9568, 94sylancom 587 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)) = ๐‘ฅ)
9693, 95eleq12d 2821 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (๐‘Š โˆˆ (๐บโ€˜(โ—ก๐บโ€˜๐‘ฅ)) โ†” โˆ… โˆˆ ๐‘ฅ))
9792, 96bitrd 279 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (โˆช dom ๐บ โˆˆ (โ—ก๐บโ€˜๐‘ฅ) โ†” โˆ… โˆˆ ๐‘ฅ))
9882, 97mtbid 324 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ยฌ โˆ… โˆˆ ๐‘ฅ)
99 onss 7769 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ On โ†’ ๐ด โІ On)
1002, 99syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐ด โІ On)
10118, 100sstrd 3987 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐น supp โˆ…) โІ On)
102101adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ (๐น supp โˆ…) โІ On)
103102sselda 3977 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ๐‘ฅ โˆˆ On)
104 on0eqel 6482 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ On โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
105103, 104syl 17 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (๐‘ฅ = โˆ… โˆจ โˆ… โˆˆ ๐‘ฅ))
106105ord 861 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ (ยฌ ๐‘ฅ = โˆ… โ†’ โˆ… โˆˆ ๐‘ฅ))
10798, 106mt3d 148 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ๐‘ฅ = โˆ…)
108 el1o 8496 . . . . . . . . . . 11 (๐‘ฅ โˆˆ 1o โ†” ๐‘ฅ = โˆ…)
109107, 108sylibr 233 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘Š = โˆ…) โˆง ๐‘ฅ โˆˆ (๐น supp โˆ…)) โ†’ ๐‘ฅ โˆˆ 1o)
110109ex 412 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ (๐‘ฅ โˆˆ (๐น supp โˆ…) โ†’ ๐‘ฅ โˆˆ 1o))
111110ssrdv 3983 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ (๐น supp โˆ…) โІ 1o)
1125, 55, 56, 57, 58, 60, 111cantnflt2 9670 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ ((ฯ‰ CNF ๐ด)โ€˜๐น) โˆˆ (ฯ‰ โ†‘o 1o))
113 oe1 8545 . . . . . . . 8 (ฯ‰ โˆˆ On โ†’ (ฯ‰ โ†‘o 1o) = ฯ‰)
1146, 113ax-mp 5 . . . . . . 7 (ฯ‰ โ†‘o 1o) = ฯ‰
115112, 114eleqtrdi 2837 . . . . . 6 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ ((ฯ‰ CNF ๐ด)โ€˜๐น) โˆˆ ฯ‰)
11654, 115eqeltrrd 2828 . . . . 5 ((๐œ‘ โˆง ๐‘Š = โˆ…) โ†’ ๐ต โˆˆ ฯ‰)
117116ex 412 . . . 4 (๐œ‘ โ†’ (๐‘Š = โˆ… โ†’ ๐ต โˆˆ ฯ‰))
118117necon3bd 2948 . . 3 (๐œ‘ โ†’ (ยฌ ๐ต โˆˆ ฯ‰ โ†’ ๐‘Š โ‰  โˆ…))
11949, 118mpd 15 . 2 (๐œ‘ โ†’ ๐‘Š โ‰  โˆ…)
120 dif1o 8501 . 2 (๐‘Š โˆˆ (On โˆ– 1o) โ†” (๐‘Š โˆˆ On โˆง ๐‘Š โ‰  โˆ…))
12142, 119, 120sylanbrc 582 1 (๐œ‘ โ†’ ๐‘Š โˆˆ (On โˆ– 1o))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2934  Vcvv 3468   โˆ– cdif 3940   โˆช cun 3941   โІ wss 3943  โˆ…c0 4317  โˆช cuni 4902   class class class wbr 5141   โ†ฆ cmpt 5224   E cep 5572   We wwe 5623  โ—กccnv 5668  dom cdm 5669  Oncon0 6358  suc csuc 6360  โŸถwf 6533  โ€“1-1-ontoโ†’wf1o 6536  โ€˜cfv 6537   Isom wiso 6538  (class class class)co 7405   โˆˆ cmpo 7407  ฯ‰com 7852   supp csupp 8146  seqฯ‰cseqom 8448  1oc1o 8460   +o coa 8464   ยทo comu 8465   โ†‘o coe 8466   finSupp cfsupp 9363  OrdIsocoi 9506   CNF ccnf 9658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-seqom 8449  df-1o 8467  df-2o 8468  df-oadd 8471  df-omul 8472  df-oexp 8473  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-oi 9507  df-cnf 9659
This theorem is referenced by:  cnfcom3  9701  cnfcom3clem  9702
  Copyright terms: Public domain W3C validator