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

Metamath Proof Explorer

Theorem infpssrlem5

Description: Lemma for infpssr . (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Hypotheses infpssrlem.a ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
infpssrlem.c ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
infpssrlem.d ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) )
infpssrlem.e ⊢ 𝐺 = ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω )
Assertion infpssrlem5 ( 𝜑 → ( 𝐴 ∈ 𝑉 → ω ≼ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 infpssrlem.a ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
2 infpssrlem.c ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
3 infpssrlem.d ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) )
4 infpssrlem.e ⊢ 𝐺 = ( rec ( ◡ 𝐹 , 𝐶 ) ↾ ω )
5 1 2 3 4 infpssrlem3 ⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝐴 )
6 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑏 ∈ 𝑐 ) → 𝜑 )
7 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑏 ∈ 𝑐 ) → 𝑐 ∈ ω )
8 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑏 ∈ 𝑐 ) → 𝑏 ∈ 𝑐 )
9 1 2 3 4 infpssrlem4 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ω ∧ 𝑏 ∈ 𝑐 ) → ( 𝐺 ‘ 𝑐 ) ≠ ( 𝐺 ‘ 𝑏 ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑏 ∈ 𝑐 ) → ( 𝐺 ‘ 𝑐 ) ≠ ( 𝐺 ‘ 𝑏 ) )
11 10 necomd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑏 ∈ 𝑐 ) → ( 𝐺 ‘ 𝑏 ) ≠ ( 𝐺 ‘ 𝑐 ) )
12 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ∈ 𝑏 ) → 𝜑 )
13 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ∈ 𝑏 ) → 𝑏 ∈ ω )
14 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ∈ 𝑏 ) → 𝑐 ∈ 𝑏 )
15 1 2 3 4 infpssrlem4 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ω ∧ 𝑐 ∈ 𝑏 ) → ( 𝐺 ‘ 𝑏 ) ≠ ( 𝐺 ‘ 𝑐 ) )
16 12 13 14 15 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ∈ 𝑏 ) → ( 𝐺 ‘ 𝑏 ) ≠ ( 𝐺 ‘ 𝑐 ) )
17 11 16 jaodan ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ ( 𝑏 ∈ 𝑐 ∨ 𝑐 ∈ 𝑏 ) ) → ( 𝐺 ‘ 𝑏 ) ≠ ( 𝐺 ‘ 𝑐 ) )
18 17 ex ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ( ( 𝑏 ∈ 𝑐 ∨ 𝑐 ∈ 𝑏 ) → ( 𝐺 ‘ 𝑏 ) ≠ ( 𝐺 ‘ 𝑐 ) ) )
19 18 necon2bd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ( ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑐 ) → ¬ ( 𝑏 ∈ 𝑐 ∨ 𝑐 ∈ 𝑏 ) ) )
20 nnord ⊢ ( 𝑏 ∈ ω → Ord 𝑏 )
21 nnord ⊢ ( 𝑐 ∈ ω → Ord 𝑐 )
22 ordtri3 ⊢ ( ( Ord 𝑏 ∧ Ord 𝑐 ) → ( 𝑏 = 𝑐 ↔ ¬ ( 𝑏 ∈ 𝑐 ∨ 𝑐 ∈ 𝑏 ) ) )
23 20 21 22 syl2an ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) → ( 𝑏 = 𝑐 ↔ ¬ ( 𝑏 ∈ 𝑐 ∨ 𝑐 ∈ 𝑏 ) ) )
24 23 adantl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ( 𝑏 = 𝑐 ↔ ¬ ( 𝑏 ∈ 𝑐 ∨ 𝑐 ∈ 𝑏 ) ) )
25 19 24 sylibrd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ( ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑐 ) → 𝑏 = 𝑐 ) )
26 25 ralrimivva ⊢ ( 𝜑 → ∀ 𝑏 ∈ ω ∀ 𝑐 ∈ ω ( ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑐 ) → 𝑏 = 𝑐 ) )
27 dff13 ⊢ ( 𝐺 : ω –1-1→ 𝐴 ↔ ( 𝐺 : ω ⟶ 𝐴 ∧ ∀ 𝑏 ∈ ω ∀ 𝑐 ∈ ω ( ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑐 ) → 𝑏 = 𝑐 ) ) )
28 5 26 27 sylanbrc ⊢ ( 𝜑 → 𝐺 : ω –1-1→ 𝐴 )
29 f1domg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐺 : ω –1-1→ 𝐴 → ω ≼ 𝐴 ) )
30 28 29 syl5com ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 → ω ≼ 𝐴 ) )