Metamath Proof Explorer

Theorem fineqvinfep

Description: A counterexample demonstrating that tz9.1 does not hold when all sets are finite and an infinite descending e. -chain exists. (Contributed by BTernaryTau, 18-Feb-2026)

Ref Expression
Hypothesis fineqvinfep.1 ⊢ 𝐴 = { ( 𝐹 ‘ ∅ ) }
Assertion fineqvinfep ( ( Fin = V ∧ 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ¬ ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) )

Proof

Step Hyp Ref Expression
1 fineqvinfep.1 ⊢ 𝐴 = { ( 𝐹 ‘ ∅ ) }
2 vex ⊢ 𝑦 ∈ V
3 eleq2 ⊢ ( Fin = V → ( 𝑦 ∈ Fin ↔ 𝑦 ∈ V ) )
4 2 3 mpbiri ⊢ ( Fin = V → 𝑦 ∈ Fin )
5 4 3ad2ant1 ⊢ ( ( Fin = V ∧ 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ Fin )
6 fveq2 ⊢ ( 𝑤 = ∅ → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ∅ ) )
7 6 eleq1d ⊢ ( 𝑤 = ∅ → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ↔ ( 𝐹 ‘ ∅ ) ∈ 𝑦 ) )
8 fveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
9 8 eleq1d ⊢ ( 𝑤 = 𝑧 → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ) )
10 fveq2 ⊢ ( 𝑤 = suc 𝑧 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ suc 𝑧 ) )
11 10 eleq1d ⊢ ( 𝑤 = suc 𝑧 → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ↔ ( 𝐹 ‘ suc 𝑧 ) ∈ 𝑦 ) )
12 simp2 ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝐴 ⊆ 𝑦 )
13 fvex ⊢ ( 𝐹 ‘ ∅ ) ∈ V
14 13 snid ⊢ ( 𝐹 ‘ ∅ ) ∈ { ( 𝐹 ‘ ∅ ) }
15 14 1 eleqtrri ⊢ ( 𝐹 ‘ ∅ ) ∈ 𝐴
16 15 a1i ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝐹 ‘ ∅ ) ∈ 𝐴 )
17 12 16 sseldd ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝐹 ‘ ∅ ) ∈ 𝑦 )
18 3simpb ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ Tr 𝑦 ) )
19 suceq ⊢ ( 𝑥 = 𝑧 → suc 𝑥 = suc 𝑧 )
20 19 fveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ suc 𝑥 ) = ( 𝐹 ‘ suc 𝑧 ) )
21 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
22 20 21 eleq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
23 22 rspcv ⊢ ( 𝑧 ∈ ω → ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
24 trel ⊢ ( Tr 𝑦 → ( ( ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ) → ( 𝐹 ‘ suc 𝑧 ) ∈ 𝑦 ) )
25 24 expd ⊢ ( Tr 𝑦 → ( ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 → ( 𝐹 ‘ suc 𝑧 ) ∈ 𝑦 ) ) )
26 25 com12 ⊢ ( ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) → ( Tr 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 → ( 𝐹 ‘ suc 𝑧 ) ∈ 𝑦 ) ) )
27 23 26 syl6 ⊢ ( 𝑧 ∈ ω → ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) → ( Tr 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 → ( 𝐹 ‘ suc 𝑧 ) ∈ 𝑦 ) ) ) )
28 27 impd ⊢ ( 𝑧 ∈ ω → ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ Tr 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 → ( 𝐹 ‘ suc 𝑧 ) ∈ 𝑦 ) ) )
29 18 28 syl5 ⊢ ( 𝑧 ∈ ω → ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 → ( 𝐹 ‘ suc 𝑧 ) ∈ 𝑦 ) ) )
30 7 9 11 17 29 finds2 ⊢ ( 𝑤 ∈ ω → ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ) )
31 30 com12 ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑤 ∈ ω → ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ) )
32 31 ralrimiv ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 )
33 32 3expib ⊢ ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) → ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ) )
34 33 adantl ⊢ ( ( 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ) )
35 f1fun ⊢ ( 𝐹 : ω –1-1→ V → Fun 𝐹 )
36 f1dm ⊢ ( 𝐹 : ω –1-1→ V → dom 𝐹 = ω )
37 36 eqimsscd ⊢ ( 𝐹 : ω –1-1→ V → ω ⊆ dom 𝐹 )
38 funimass4 ⊢ ( ( Fun 𝐹 ∧ ω ⊆ dom 𝐹 ) → ( ( 𝐹 “ ω ) ⊆ 𝑦 ↔ ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ) )
39 35 37 38 syl2anc ⊢ ( 𝐹 : ω –1-1→ V → ( ( 𝐹 “ ω ) ⊆ 𝑦 ↔ ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ) )
40 39 adantr ⊢ ( ( 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 “ ω ) ⊆ 𝑦 ↔ ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ 𝑦 ) )
41 34 40 sylibrd ⊢ ( ( 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝐹 “ ω ) ⊆ 𝑦 ) )
42 ominf ⊢ ¬ ω ∈ Fin
43 f1fn ⊢ ( 𝐹 : ω –1-1→ V → 𝐹 Fn ω )
44 fnima ⊢ ( 𝐹 Fn ω → ( 𝐹 “ ω ) = ran 𝐹 )
45 43 44 syl ⊢ ( 𝐹 : ω –1-1→ V → ( 𝐹 “ ω ) = ran 𝐹 )
46 45 eqimsscd ⊢ ( 𝐹 : ω –1-1→ V → ran 𝐹 ⊆ ( 𝐹 “ ω ) )
47 f1ssr ⊢ ( ( 𝐹 : ω –1-1→ V ∧ ran 𝐹 ⊆ ( 𝐹 “ ω ) ) → 𝐹 : ω –1-1→ ( 𝐹 “ ω ) )
48 46 47 mpdan ⊢ ( 𝐹 : ω –1-1→ V → 𝐹 : ω –1-1→ ( 𝐹 “ ω ) )
49 f1fi ⊢ ( ( ( 𝐹 “ ω ) ∈ Fin ∧ 𝐹 : ω –1-1→ ( 𝐹 “ ω ) ) → ω ∈ Fin )
50 48 49 sylan2 ⊢ ( ( ( 𝐹 “ ω ) ∈ Fin ∧ 𝐹 : ω –1-1→ V ) → ω ∈ Fin )
51 50 ancoms ⊢ ( ( 𝐹 : ω –1-1→ V ∧ ( 𝐹 “ ω ) ∈ Fin ) → ω ∈ Fin )
52 42 51 mto ⊢ ¬ ( 𝐹 : ω –1-1→ V ∧ ( 𝐹 “ ω ) ∈ Fin )
53 52 imnani ⊢ ( 𝐹 : ω –1-1→ V → ¬ ( 𝐹 “ ω ) ∈ Fin )
54 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝐹 “ ω ) ⊆ 𝑦 ) → ( 𝐹 “ ω ) ∈ Fin )
55 54 ancoms ⊢ ( ( ( 𝐹 “ ω ) ⊆ 𝑦 ∧ 𝑦 ∈ Fin ) → ( 𝐹 “ ω ) ∈ Fin )
56 55 con3i ⊢ ( ¬ ( 𝐹 “ ω ) ∈ Fin → ¬ ( ( 𝐹 “ ω ) ⊆ 𝑦 ∧ 𝑦 ∈ Fin ) )
57 imnan ⊢ ( ( ( 𝐹 “ ω ) ⊆ 𝑦 → ¬ 𝑦 ∈ Fin ) ↔ ¬ ( ( 𝐹 “ ω ) ⊆ 𝑦 ∧ 𝑦 ∈ Fin ) )
58 56 57 sylibr ⊢ ( ¬ ( 𝐹 “ ω ) ∈ Fin → ( ( 𝐹 “ ω ) ⊆ 𝑦 → ¬ 𝑦 ∈ Fin ) )
59 53 58 syl ⊢ ( 𝐹 : ω –1-1→ V → ( ( 𝐹 “ ω ) ⊆ 𝑦 → ¬ 𝑦 ∈ Fin ) )
60 59 adantr ⊢ ( ( 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 “ ω ) ⊆ 𝑦 → ¬ 𝑦 ∈ Fin ) )
61 41 60 syld ⊢ ( ( 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ¬ 𝑦 ∈ Fin ) )
62 61 3adant1 ⊢ ( ( Fin = V ∧ 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ¬ 𝑦 ∈ Fin ) )
63 5 62 mt2d ⊢ ( ( Fin = V ∧ 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ¬ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) )
64 63 nexdv ⊢ ( ( Fin = V ∧ 𝐹 : ω –1-1→ V ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ¬ ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) )