Metamath Proof Explorer


Theorem inf3lemd

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 inf3lemd ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊆ 𝑥 )

Proof

Step Hyp Ref Expression
1 inf3lem.1 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 𝐴 ∈ V
4 inf3lem.4 𝐵 ∈ V
5 fveq2 ( 𝐴 = ∅ → ( 𝐹𝐴 ) = ( 𝐹 ‘ ∅ ) )
6 1 2 3 4 inf3lemb ( 𝐹 ‘ ∅ ) = ∅
7 5 6 eqtrdi ( 𝐴 = ∅ → ( 𝐹𝐴 ) = ∅ )
8 0ss ∅ ⊆ 𝑥
9 7 8 eqsstrdi ( 𝐴 = ∅ → ( 𝐹𝐴 ) ⊆ 𝑥 )
10 9 a1d ( 𝐴 = ∅ → ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊆ 𝑥 ) )
11 nnsuc ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑣 ∈ ω 𝐴 = suc 𝑣 )
12 vex 𝑣 ∈ V
13 1 2 12 4 inf3lemc ( 𝑣 ∈ ω → ( 𝐹 ‘ suc 𝑣 ) = ( 𝐺 ‘ ( 𝐹𝑣 ) ) )
14 13 eleq2d ( 𝑣 ∈ ω → ( 𝑢 ∈ ( 𝐹 ‘ suc 𝑣 ) ↔ 𝑢 ∈ ( 𝐺 ‘ ( 𝐹𝑣 ) ) ) )
15 vex 𝑢 ∈ V
16 fvex ( 𝐹𝑣 ) ∈ V
17 1 2 15 16 inf3lema ( 𝑢 ∈ ( 𝐺 ‘ ( 𝐹𝑣 ) ) ↔ ( 𝑢𝑥 ∧ ( 𝑢𝑥 ) ⊆ ( 𝐹𝑣 ) ) )
18 17 simplbi ( 𝑢 ∈ ( 𝐺 ‘ ( 𝐹𝑣 ) ) → 𝑢𝑥 )
19 14 18 syl6bi ( 𝑣 ∈ ω → ( 𝑢 ∈ ( 𝐹 ‘ suc 𝑣 ) → 𝑢𝑥 ) )
20 19 ssrdv ( 𝑣 ∈ ω → ( 𝐹 ‘ suc 𝑣 ) ⊆ 𝑥 )
21 fveq2 ( 𝐴 = suc 𝑣 → ( 𝐹𝐴 ) = ( 𝐹 ‘ suc 𝑣 ) )
22 21 sseq1d ( 𝐴 = suc 𝑣 → ( ( 𝐹𝐴 ) ⊆ 𝑥 ↔ ( 𝐹 ‘ suc 𝑣 ) ⊆ 𝑥 ) )
23 20 22 syl5ibrcom ( 𝑣 ∈ ω → ( 𝐴 = suc 𝑣 → ( 𝐹𝐴 ) ⊆ 𝑥 ) )
24 23 rexlimiv ( ∃ 𝑣 ∈ ω 𝐴 = suc 𝑣 → ( 𝐹𝐴 ) ⊆ 𝑥 )
25 11 24 syl ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ( 𝐹𝐴 ) ⊆ 𝑥 )
26 25 expcom ( 𝐴 ≠ ∅ → ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊆ 𝑥 ) )
27 10 26 pm2.61ine ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊆ 𝑥 )