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 𝐴 ) ) )