Metamath Proof Explorer

Theorem inf3lem1

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
inf3lem.3 ⊢ 𝐴 ∈ V
inf3lem.4 ⊢ 𝐵 ∈ V
Assertion inf3lem1 ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐴 ) )

Proof

Step Hyp Ref Expression
1 inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 ⊢ 𝐴 ∈ V
4 inf3lem.4 ⊢ 𝐵 ∈ V
5 fveq2 ⊢ ( 𝑣 = ∅ → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ ∅ ) )
6 suceq ⊢ ( 𝑣 = ∅ → suc 𝑣 = suc ∅ )
7 6 fveq2d ⊢ ( 𝑣 = ∅ → ( 𝐹 ‘ suc 𝑣 ) = ( 𝐹 ‘ suc ∅ ) )
8 5 7 sseq12d ⊢ ( 𝑣 = ∅ → ( ( 𝐹 ‘ 𝑣 ) ⊆ ( 𝐹 ‘ suc 𝑣 ) ↔ ( 𝐹 ‘ ∅ ) ⊆ ( 𝐹 ‘ suc ∅ ) ) )
9 fveq2 ⊢ ( 𝑣 = 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) )
10 suceq ⊢ ( 𝑣 = 𝑢 → suc 𝑣 = suc 𝑢 )
11 10 fveq2d ⊢ ( 𝑣 = 𝑢 → ( 𝐹 ‘ suc 𝑣 ) = ( 𝐹 ‘ suc 𝑢 ) )
12 9 11 sseq12d ⊢ ( 𝑣 = 𝑢 → ( ( 𝐹 ‘ 𝑣 ) ⊆ ( 𝐹 ‘ suc 𝑣 ) ↔ ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) )
13 fveq2 ⊢ ( 𝑣 = suc 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ suc 𝑢 ) )
14 suceq ⊢ ( 𝑣 = suc 𝑢 → suc 𝑣 = suc suc 𝑢 )
15 14 fveq2d ⊢ ( 𝑣 = suc 𝑢 → ( 𝐹 ‘ suc 𝑣 ) = ( 𝐹 ‘ suc suc 𝑢 ) )
16 13 15 sseq12d ⊢ ( 𝑣 = suc 𝑢 → ( ( 𝐹 ‘ 𝑣 ) ⊆ ( 𝐹 ‘ suc 𝑣 ) ↔ ( 𝐹 ‘ suc 𝑢 ) ⊆ ( 𝐹 ‘ suc suc 𝑢 ) ) )
17 fveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) )
18 suceq ⊢ ( 𝑣 = 𝐴 → suc 𝑣 = suc 𝐴 )
19 18 fveq2d ⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ suc 𝑣 ) = ( 𝐹 ‘ suc 𝐴 ) )
20 17 19 sseq12d ⊢ ( 𝑣 = 𝐴 → ( ( 𝐹 ‘ 𝑣 ) ⊆ ( 𝐹 ‘ suc 𝑣 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐴 ) ) )
21 1 2 3 3 inf3lemb ⊢ ( 𝐹 ‘ ∅ ) = ∅
22 0ss ⊢ ∅ ⊆ ( 𝐹 ‘ suc ∅ )
23 21 22 eqsstri ⊢ ( 𝐹 ‘ ∅ ) ⊆ ( 𝐹 ‘ suc ∅ )
24 sstr2 ⊢ ( ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) → ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) → ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) )
25 24 com12 ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) → ( ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) → ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) )
26 25 anim2d ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) ) → ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) ) )
27 vex ⊢ 𝑢 ∈ V
28 1 2 27 3 inf3lemc ⊢ ( 𝑢 ∈ ω → ( 𝐹 ‘ suc 𝑢 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) )
29 28 eleq2d ⊢ ( 𝑢 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝑢 ) ↔ 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) ) )
30 vex ⊢ 𝑣 ∈ V
31 fvex ⊢ ( 𝐹 ‘ 𝑢 ) ∈ V
32 1 2 30 31 inf3lema ⊢ ( 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) ) )
33 29 32 syl6bb ⊢ ( 𝑢 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝑢 ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) ) ) )
34 peano2b ⊢ ( 𝑢 ∈ ω ↔ suc 𝑢 ∈ ω )
35 27 sucex ⊢ suc 𝑢 ∈ V
36 1 2 35 3 inf3lemc ⊢ ( suc 𝑢 ∈ ω → ( 𝐹 ‘ suc suc 𝑢 ) = ( 𝐺 ‘ ( 𝐹 ‘ suc 𝑢 ) ) )
37 34 36 sylbi ⊢ ( 𝑢 ∈ ω → ( 𝐹 ‘ suc suc 𝑢 ) = ( 𝐺 ‘ ( 𝐹 ‘ suc 𝑢 ) ) )
38 37 eleq2d ⊢ ( 𝑢 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc suc 𝑢 ) ↔ 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ suc 𝑢 ) ) ) )
39 fvex ⊢ ( 𝐹 ‘ suc 𝑢 ) ∈ V
40 1 2 30 39 inf3lema ⊢ ( 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ suc 𝑢 ) ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) )
41 38 40 syl6bb ⊢ ( 𝑢 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc suc 𝑢 ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) ) )
42 33 41 imbi12d ⊢ ( 𝑢 ∈ ω → ( ( 𝑣 ∈ ( 𝐹 ‘ suc 𝑢 ) → 𝑣 ∈ ( 𝐹 ‘ suc suc 𝑢 ) ) ↔ ( ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) ) → ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) ) ) )
43 26 42 syl5ibr ⊢ ( 𝑢 ∈ ω → ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝑢 ) → 𝑣 ∈ ( 𝐹 ‘ suc suc 𝑢 ) ) ) )
44 43 imp ⊢ ( ( 𝑢 ∈ ω ∧ ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝑢 ) → 𝑣 ∈ ( 𝐹 ‘ suc suc 𝑢 ) ) )
45 44 ssrdv ⊢ ( ( 𝑢 ∈ ω ∧ ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) ) → ( 𝐹 ‘ suc 𝑢 ) ⊆ ( 𝐹 ‘ suc suc 𝑢 ) )
46 45 ex ⊢ ( 𝑢 ∈ ω → ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ suc 𝑢 ) → ( 𝐹 ‘ suc 𝑢 ) ⊆ ( 𝐹 ‘ suc suc 𝑢 ) ) )
47 8 12 16 20 23 46 finds ⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐴 ) )