Metamath Proof Explorer


Theorem inf3lem4

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

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

Proof

Step Hyp Ref Expression
1 inf3lem.1 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 𝐴 ∈ V
4 inf3lem.4 𝐵 ∈ V
5 1 2 3 4 inf3lem1 ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐴 ) )
6 5 a1i ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐴 ) ) )
7 1 2 3 4 inf3lem3 ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
8 6 7 jcad ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐴 ∈ ω → ( ( 𝐹𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐴 ) ∧ ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) )
9 df-pss ( ( 𝐹𝐴 ) ⊊ ( 𝐹 ‘ suc 𝐴 ) ↔ ( ( 𝐹𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐴 ) ∧ ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
10 8 9 syl6ibr ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊊ ( 𝐹 ‘ suc 𝐴 ) ) )