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	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 → ω ≼ 𝐴 ) )