Metamath Proof Explorer


Theorem inf3lem5

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 inf3lem5 ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 inf3lem.1 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 𝐴 ∈ V
4 inf3lem.4 𝐵 ∈ V
5 elnn ( ( 𝐵𝐴𝐴 ∈ ω ) → 𝐵 ∈ ω )
6 5 ancoms ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → 𝐵 ∈ ω )
7 nnord ( 𝐴 ∈ ω → Ord 𝐴 )
8 ordsucss ( Ord 𝐴 → ( 𝐵𝐴 → suc 𝐵𝐴 ) )
9 7 8 syl ( 𝐴 ∈ ω → ( 𝐵𝐴 → suc 𝐵𝐴 ) )
10 9 adantr ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵𝐴 → suc 𝐵𝐴 ) )
11 peano2b ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω )
12 fveq2 ( 𝑣 = suc 𝐵 → ( 𝐹𝑣 ) = ( 𝐹 ‘ suc 𝐵 ) )
13 12 psseq2d ( 𝑣 = suc 𝐵 → ( ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ↔ ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
14 13 imbi2d ( 𝑣 = suc 𝐵 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) ) )
15 fveq2 ( 𝑣 = 𝑢 → ( 𝐹𝑣 ) = ( 𝐹𝑢 ) )
16 15 psseq2d ( 𝑣 = 𝑢 → ( ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ↔ ( 𝐹𝐵 ) ⊊ ( 𝐹𝑢 ) ) )
17 16 imbi2d ( 𝑣 = 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝑢 ) ) ) )
18 fveq2 ( 𝑣 = suc 𝑢 → ( 𝐹𝑣 ) = ( 𝐹 ‘ suc 𝑢 ) )
19 18 psseq2d ( 𝑣 = suc 𝑢 → ( ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ↔ ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) )
20 19 imbi2d ( 𝑣 = suc 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
21 fveq2 ( 𝑣 = 𝐴 → ( 𝐹𝑣 ) = ( 𝐹𝐴 ) )
22 21 psseq2d ( 𝑣 = 𝐴 → ( ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ↔ ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) )
23 22 imbi2d ( 𝑣 = 𝐴 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) ) )
24 1 2 4 4 inf3lem4 ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐵 ∈ ω → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
25 24 com12 ( 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
26 11 25 sylbir ( suc 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
27 vex 𝑢 ∈ V
28 1 2 27 4 inf3lem4 ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝑢 ∈ ω → ( 𝐹𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) )
29 psstr ( ( ( 𝐹𝐵 ) ⊊ ( 𝐹𝑢 ) ∧ ( 𝐹𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) )
30 29 expcom ( ( 𝐹𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) → ( ( 𝐹𝐵 ) ⊊ ( 𝐹𝑢 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) )
31 28 30 syl6com ( 𝑢 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( ( 𝐹𝐵 ) ⊊ ( 𝐹𝑢 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
32 31 a2d ( 𝑢 ∈ ω → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝑢 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
33 32 ad2antrr ( ( ( 𝑢 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ suc 𝐵𝑢 ) → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝑢 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
34 14 17 20 23 26 33 findsg ( ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ suc 𝐵𝐴 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) )
35 34 ex ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) → ( suc 𝐵𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) ) )
36 11 35 sylan2b ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐵𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) ) )
37 10 36 syld ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) ) )
38 37 impancom ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ( 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) ) )
39 6 38 mpd ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) )
40 39 com12 ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ( 𝐹𝐵 ) ⊊ ( 𝐹𝐴 ) ) )