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 ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
fin23lem.f ⊢ ( 𝜑 → ℎ : ω –1-1→ V )
fin23lem.g ⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
fin23lem.h ⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
fin23lem.i ⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
Assertion fin23lem39 ( 𝜑 → ¬ 𝐺 ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 fin23lem33.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2 fin23lem.f ⊢ ( 𝜑 → ℎ : ω –1-1→ V )
3 fin23lem.g ⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
4 fin23lem.h ⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
5 fin23lem.i ⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
6 1 2 3 4 5 fin23lem38 ⊢ ( 𝜑 → ¬ ∩ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) )
7 1 2 3 4 5 fin23lem35 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝑒 ) ⊊ ∪ ran ( 𝑌 ‘ 𝑒 ) )
8 7 pssssd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝑒 ) ⊆ ∪ ran ( 𝑌 ‘ 𝑒 ) )
9 peano2 ⊢ ( 𝑒 ∈ ω → suc 𝑒 ∈ ω )
10 fveq2 ⊢ ( 𝑐 = suc 𝑒 → ( 𝑌 ‘ 𝑐 ) = ( 𝑌 ‘ suc 𝑒 ) )
11 10 rneqd ⊢ ( 𝑐 = suc 𝑒 → ran ( 𝑌 ‘ 𝑐 ) = ran ( 𝑌 ‘ suc 𝑒 ) )
12 11 unieqd ⊢ ( 𝑐 = suc 𝑒 → ∪ ran ( 𝑌 ‘ 𝑐 ) = ∪ ran ( 𝑌 ‘ suc 𝑒 ) )
13 eqid ⊢ ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) )
14 fvex ⊢ ( 𝑌 ‘ suc 𝑒 ) ∈ V
15 14 rnex ⊢ ran ( 𝑌 ‘ suc 𝑒 ) ∈ V
16 15 uniex ⊢ ∪ ran ( 𝑌 ‘ suc 𝑒 ) ∈ V
17 12 13 16 fvmpt ⊢ ( suc 𝑒 ∈ ω → ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) = ∪ ran ( 𝑌 ‘ suc 𝑒 ) )
18 9 17 syl ⊢ ( 𝑒 ∈ ω → ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) = ∪ ran ( 𝑌 ‘ suc 𝑒 ) )
19 fveq2 ⊢ ( 𝑐 = 𝑒 → ( 𝑌 ‘ 𝑐 ) = ( 𝑌 ‘ 𝑒 ) )
20 19 rneqd ⊢ ( 𝑐 = 𝑒 → ran ( 𝑌 ‘ 𝑐 ) = ran ( 𝑌 ‘ 𝑒 ) )
21 20 unieqd ⊢ ( 𝑐 = 𝑒 → ∪ ran ( 𝑌 ‘ 𝑐 ) = ∪ ran ( 𝑌 ‘ 𝑒 ) )
22 fvex ⊢ ( 𝑌 ‘ 𝑒 ) ∈ V
23 22 rnex ⊢ ran ( 𝑌 ‘ 𝑒 ) ∈ V
24 23 uniex ⊢ ∪ ran ( 𝑌 ‘ 𝑒 ) ∈ V
25 21 13 24 fvmpt ⊢ ( 𝑒 ∈ ω → ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) = ∪ ran ( 𝑌 ‘ 𝑒 ) )
26 18 25 sseq12d ⊢ ( 𝑒 ∈ ω → ( ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) ↔ ∪ ran ( 𝑌 ‘ suc 𝑒 ) ⊆ ∪ ran ( 𝑌 ‘ 𝑒 ) ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ω ) → ( ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) ↔ ∪ ran ( 𝑌 ‘ suc 𝑒 ) ⊆ ∪ ran ( 𝑌 ‘ 𝑒 ) ) )
28 8 27 mpbird ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ω ) → ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ ω ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) → ∀ 𝑒 ∈ ω ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) )
31 fveq1 ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ( 𝑑 ‘ suc 𝑒 ) = ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) )
32 fveq1 ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ( 𝑑 ‘ 𝑒 ) = ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) )
33 31 32 sseq12d ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ( ( 𝑑 ‘ suc 𝑒 ) ⊆ ( 𝑑 ‘ 𝑒 ) ↔ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) ) )
34 33 ralbidv ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ( ∀ 𝑒 ∈ ω ( 𝑑 ‘ suc 𝑒 ) ⊆ ( 𝑑 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ ω ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) ) )
35 rneq ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ran 𝑑 = ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) )
36 35 inteqd ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ∩ ran 𝑑 = ∩ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) )
37 36 35 eleq12d ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ( ∩ ran 𝑑 ∈ ran 𝑑 ↔ ∩ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ) )
38 34 37 imbi12d ⊢ ( 𝑑 = ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) → ( ( ∀ 𝑒 ∈ ω ( 𝑑 ‘ suc 𝑒 ) ⊆ ( 𝑑 ‘ 𝑒 ) → ∩ ran 𝑑 ∈ ran 𝑑 ) ↔ ( ∀ 𝑒 ∈ ω ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) → ∩ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ) ) )
39 1 isfin3ds ⊢ ( 𝐺 ∈ 𝐹 → ( 𝐺 ∈ 𝐹 ↔ ∀ 𝑑 ∈ ( 𝒫 𝐺 ↑m ω ) ( ∀ 𝑒 ∈ ω ( 𝑑 ‘ suc 𝑒 ) ⊆ ( 𝑑 ‘ 𝑒 ) → ∩ ran 𝑑 ∈ ran 𝑑 ) ) )
40 39 ibi ⊢ ( 𝐺 ∈ 𝐹 → ∀ 𝑑 ∈ ( 𝒫 𝐺 ↑m ω ) ( ∀ 𝑒 ∈ ω ( 𝑑 ‘ suc 𝑒 ) ⊆ ( 𝑑 ‘ 𝑒 ) → ∩ ran 𝑑 ∈ ran 𝑑 ) )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) → ∀ 𝑑 ∈ ( 𝒫 𝐺 ↑m ω ) ( ∀ 𝑒 ∈ ω ( 𝑑 ‘ suc 𝑒 ) ⊆ ( 𝑑 ‘ 𝑒 ) → ∩ ran 𝑑 ∈ ran 𝑑 ) )
42 1 2 3 4 5 fin23lem34 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ω ) → ( ( 𝑌 ‘ 𝑐 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑐 ) ⊆ 𝐺 ) )
43 42 simprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ω ) → ∪ ran ( 𝑌 ‘ 𝑐 ) ⊆ 𝐺 )
44 43 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑐 ∈ ω ) → ∪ ran ( 𝑌 ‘ 𝑐 ) ⊆ 𝐺 )
45 elpw2g ⊢ ( 𝐺 ∈ 𝐹 → ( ∪ ran ( 𝑌 ‘ 𝑐 ) ∈ 𝒫 𝐺 ↔ ∪ ran ( 𝑌 ‘ 𝑐 ) ⊆ 𝐺 ) )
46 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑐 ∈ ω ) → ( ∪ ran ( 𝑌 ‘ 𝑐 ) ∈ 𝒫 𝐺 ↔ ∪ ran ( 𝑌 ‘ 𝑐 ) ⊆ 𝐺 ) )
47 44 46 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑐 ∈ ω ) → ∪ ran ( 𝑌 ‘ 𝑐 ) ∈ 𝒫 𝐺 )
48 47 fmpttd ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) → ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) : ω ⟶ 𝒫 𝐺 )
49 pwexg ⊢ ( 𝐺 ∈ 𝐹 → 𝒫 𝐺 ∈ V )
50 vex ⊢ ℎ ∈ V
51 f1f ⊢ ( ℎ : ω –1-1→ V → ℎ : ω ⟶ V )
52 dmfex ⊢ ( ( ℎ ∈ V ∧ ℎ : ω ⟶ V ) → ω ∈ V )
53 50 51 52 sylancr ⊢ ( ℎ : ω –1-1→ V → ω ∈ V )
54 2 53 syl ⊢ ( 𝜑 → ω ∈ V )
55 elmapg ⊢ ( ( 𝒫 𝐺 ∈ V ∧ ω ∈ V ) → ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ( 𝒫 𝐺 ↑m ω ) ↔ ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) : ω ⟶ 𝒫 𝐺 ) )
56 49 54 55 syl2anr ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ( 𝒫 𝐺 ↑m ω ) ↔ ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) : ω ⟶ 𝒫 𝐺 ) )
57 48 56 mpbird ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) → ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ( 𝒫 𝐺 ↑m ω ) )
58 38 41 57 rspcdva ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) → ( ∀ 𝑒 ∈ ω ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ suc 𝑒 ) ⊆ ( ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ‘ 𝑒 ) → ∩ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ) )
59 30 58 mpd ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐹 ) → ∩ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) ∈ ran ( 𝑐 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑐 ) ) )
60 6 59 mtand ⊢ ( 𝜑 → ¬ 𝐺 ∈ 𝐹 )