inf3lem7

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex . (Contributed by NM, 29-Oct-1996) (Proof shortened by Mario Carneiro, 19-Jan-2013)

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

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	inf3lem6	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → 𝐹 : ω –1-1→ 𝒫 𝑥 )
6		vpwex	⊢ 𝒫 𝑥 ∈ V
7		f1dmex	⊢ ( ( 𝐹 : ω –1-1→ 𝒫 𝑥 ∧ 𝒫 𝑥 ∈ V ) → ω ∈ V )
8	5 6 7	sylancl	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ω ∈ V )

Metamath Proof Explorer

Theorem inf3lem7

Proof