This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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