Metamath Proof Explorer

Theorem fin23lem39

Description: Lemma for fin23 . Thus, we have that g could not have been in F after all. (Contributed by Stefan O'Rear, 4-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f ⊢F=g|∀a∈𝒫gω∀x∈ωa⁡suc⁡x⊆a⁡x→⋂ran⁡a∈ran⁡a
fin23lem.f ⊢φ→h:ω⟶1-1V
fin23lem.g ⊢φ→⋃ran⁡h⊆G
fin23lem.h ⊢φ→∀jj:ω⟶1-1V∧⋃ran⁡j⊆G→i⁡j:ω⟶1-1V∧⋃ran⁡i⁡j⊂⋃ran⁡j
fin23lem.i ⊢Y=rec⁡ih↾ω
Assertion fin23lem39 ⊢φ→¬G∈F

Proof

Step Hyp Ref Expression
1 fin23lem33.f ⊢F=g|∀a∈𝒫gω∀x∈ωa⁡suc⁡x⊆a⁡x→⋂ran⁡a∈ran⁡a
2 fin23lem.f ⊢φ→h:ω⟶1-1V
3 fin23lem.g ⊢φ→⋃ran⁡h⊆G
4 fin23lem.h ⊢φ→∀jj:ω⟶1-1V∧⋃ran⁡j⊆G→i⁡j:ω⟶1-1V∧⋃ran⁡i⁡j⊂⋃ran⁡j
5 fin23lem.i ⊢Y=rec⁡ih↾ω
6 1 2 3 4 5 fin23lem38 ⊢φ→¬⋂ran⁡c∈ω⟼⋃ran⁡Y⁡c∈ran⁡c∈ω⟼⋃ran⁡Y⁡c
7 1 2 3 4 5 fin23lem35 ⊢φ∧e∈ω→⋃ran⁡Y⁡suc⁡e⊂⋃ran⁡Y⁡e
8 7 pssssd ⊢φ∧e∈ω→⋃ran⁡Y⁡suc⁡e⊆⋃ran⁡Y⁡e
9 peano2 ⊢e∈ω→suc⁡e∈ω
10 fveq2 ⊢c=suc⁡e→Y⁡c=Y⁡suc⁡e
11 10 rneqd ⊢c=suc⁡e→ran⁡Y⁡c=ran⁡Y⁡suc⁡e
12 11 unieqd ⊢c=suc⁡e→⋃ran⁡Y⁡c=⋃ran⁡Y⁡suc⁡e
13 eqid ⊢c∈ω⟼⋃ran⁡Y⁡c=c∈ω⟼⋃ran⁡Y⁡c
14 fvex ⊢Y⁡suc⁡e∈V
15 14 rnex ⊢ran⁡Y⁡suc⁡e∈V
16 15 uniex ⊢⋃ran⁡Y⁡suc⁡e∈V
17 12 13 16 fvmpt ⊢suc⁡e∈ω→c∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e=⋃ran⁡Y⁡suc⁡e
18 9 17 syl ⊢e∈ω→c∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e=⋃ran⁡Y⁡suc⁡e
19 fveq2 ⊢c=e→Y⁡c=Y⁡e
20 19 rneqd ⊢c=e→ran⁡Y⁡c=ran⁡Y⁡e
21 20 unieqd ⊢c=e→⋃ran⁡Y⁡c=⋃ran⁡Y⁡e
22 fvex ⊢Y⁡e∈V
23 22 rnex ⊢ran⁡Y⁡e∈V
24 23 uniex ⊢⋃ran⁡Y⁡e∈V
25 21 13 24 fvmpt ⊢e∈ω→c∈ω⟼⋃ran⁡Y⁡c⁡e=⋃ran⁡Y⁡e
26 18 25 sseq12d ⊢e∈ω→c∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e↔⋃ran⁡Y⁡suc⁡e⊆⋃ran⁡Y⁡e
27 26 adantl ⊢φ∧e∈ω→c∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e↔⋃ran⁡Y⁡suc⁡e⊆⋃ran⁡Y⁡e
28 8 27 mpbird ⊢φ∧e∈ω→c∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e
29 28 ralrimiva ⊢φ→∀e∈ωc∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e
30 29 adantr ⊢φ∧G∈F→∀e∈ωc∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e
31 fveq1 ⊢d=c∈ω⟼⋃ran⁡Y⁡c→d⁡suc⁡e=c∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e
32 fveq1 ⊢d=c∈ω⟼⋃ran⁡Y⁡c→d⁡e=c∈ω⟼⋃ran⁡Y⁡c⁡e
33 31 32 sseq12d ⊢d=c∈ω⟼⋃ran⁡Y⁡c→d⁡suc⁡e⊆d⁡e↔c∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e
34 33 ralbidv ⊢d=c∈ω⟼⋃ran⁡Y⁡c→∀e∈ωd⁡suc⁡e⊆d⁡e↔∀e∈ωc∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e
35 rneq ⊢d=c∈ω⟼⋃ran⁡Y⁡c→ran⁡d=ran⁡c∈ω⟼⋃ran⁡Y⁡c
36 35 inteqd ⊢d=c∈ω⟼⋃ran⁡Y⁡c→⋂ran⁡d=⋂ran⁡c∈ω⟼⋃ran⁡Y⁡c
37 36 35 eleq12d ⊢d=c∈ω⟼⋃ran⁡Y⁡c→⋂ran⁡d∈ran⁡d↔⋂ran⁡c∈ω⟼⋃ran⁡Y⁡c∈ran⁡c∈ω⟼⋃ran⁡Y⁡c
38 34 37 imbi12d ⊢d=c∈ω⟼⋃ran⁡Y⁡c→∀e∈ωd⁡suc⁡e⊆d⁡e→⋂ran⁡d∈ran⁡d↔∀e∈ωc∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e→⋂ran⁡c∈ω⟼⋃ran⁡Y⁡c∈ran⁡c∈ω⟼⋃ran⁡Y⁡c
39 1 isfin3ds ⊢G∈F→G∈F↔∀d∈𝒫Gω∀e∈ωd⁡suc⁡e⊆d⁡e→⋂ran⁡d∈ran⁡d
40 39 ibi ⊢G∈F→∀d∈𝒫Gω∀e∈ωd⁡suc⁡e⊆d⁡e→⋂ran⁡d∈ran⁡d
41 40 adantl ⊢φ∧G∈F→∀d∈𝒫Gω∀e∈ωd⁡suc⁡e⊆d⁡e→⋂ran⁡d∈ran⁡d
42 1 2 3 4 5 fin23lem34 ⊢φ∧c∈ω→Y⁡c:ω⟶1-1V∧⋃ran⁡Y⁡c⊆G
43 42 simprd ⊢φ∧c∈ω→⋃ran⁡Y⁡c⊆G
44 43 adantlr ⊢φ∧G∈F∧c∈ω→⋃ran⁡Y⁡c⊆G
45 elpw2g ⊢G∈F→⋃ran⁡Y⁡c∈𝒫G↔⋃ran⁡Y⁡c⊆G
46 45 ad2antlr ⊢φ∧G∈F∧c∈ω→⋃ran⁡Y⁡c∈𝒫G↔⋃ran⁡Y⁡c⊆G
47 44 46 mpbird ⊢φ∧G∈F∧c∈ω→⋃ran⁡Y⁡c∈𝒫G
48 47 fmpttd ⊢φ∧G∈F→c∈ω⟼⋃ran⁡Y⁡c:ω⟶𝒫G
49 pwexg ⊢G∈F→𝒫G∈V
50 vex ⊢h∈V
51 f1f ⊢h:ω⟶1-1V→h:ω⟶V
52 dmfex ⊢h∈V∧h:ω⟶V→ω∈V
53 50 51 52 sylancr ⊢h:ω⟶1-1V→ω∈V
54 2 53 syl ⊢φ→ω∈V
55 elmapg ⊢𝒫G∈V∧ω∈V→c∈ω⟼⋃ran⁡Y⁡c∈𝒫Gω↔c∈ω⟼⋃ran⁡Y⁡c:ω⟶𝒫G
56 49 54 55 syl2anr ⊢φ∧G∈F→c∈ω⟼⋃ran⁡Y⁡c∈𝒫Gω↔c∈ω⟼⋃ran⁡Y⁡c:ω⟶𝒫G
57 48 56 mpbird ⊢φ∧G∈F→c∈ω⟼⋃ran⁡Y⁡c∈𝒫Gω
58 38 41 57 rspcdva ⊢φ∧G∈F→∀e∈ωc∈ω⟼⋃ran⁡Y⁡c⁡suc⁡e⊆c∈ω⟼⋃ran⁡Y⁡c⁡e→⋂ran⁡c∈ω⟼⋃ran⁡Y⁡c∈ran⁡c∈ω⟼⋃ran⁡Y⁡c
59 30 58 mpd ⊢φ∧G∈F→⋂ran⁡c∈ω⟼⋃ran⁡Y⁡c∈ran⁡c∈ω⟼⋃ran⁡Y⁡c
60 6 59 mtand ⊢φ→¬G∈F