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	biimtrdi	⊢ ( 𝑣 ∈ ω → ( 𝑢 ∈ ( 𝐹 ‘ 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	⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 )