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 bitrdi ( 𝑢 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ 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 bitrdi ( 𝑢 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ 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 𝐴 ) )