Metamath Proof Explorer

Theorem infpssrlem5

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

Ref Expression
Hypotheses infpssrlem.a ⊢ φ → B ⊆ A
infpssrlem.c ⊢ φ → F : B ⟶ 1-1 onto A
infpssrlem.d ⊢ φ → C ∈ A ∖ B
infpssrlem.e ⊢ G = rec ⁡ F -1 C ↾ ω
Assertion infpssrlem5 ⊢ φ → A ∈ V → ω ≼ A

Proof

Step Hyp Ref Expression
1 infpssrlem.a ⊢ φ → B ⊆ A
2 infpssrlem.c ⊢ φ → F : B ⟶ 1-1 onto A
3 infpssrlem.d ⊢ φ → C ∈ A ∖ B
4 infpssrlem.e ⊢ G = rec ⁡ F -1 C ↾ ω
5 1 2 3 4 infpssrlem3 ⊢ φ → G : ω ⟶ A
6 simpll ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ b ∈ c → φ
7 simplrr ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ b ∈ c → c ∈ ω
8 simpr ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ b ∈ c → b ∈ c
9 1 2 3 4 infpssrlem4 ⊢ φ ∧ c ∈ ω ∧ b ∈ c → G ⁡ c ≠ G ⁡ b
10 6 7 8 9 syl3anc ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ b ∈ c → G ⁡ c ≠ G ⁡ b
11 10 necomd ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ b ∈ c → G ⁡ b ≠ G ⁡ c
12 simpll ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ c ∈ b → φ
13 simplrl ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ c ∈ b → b ∈ ω
14 simpr ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ c ∈ b → c ∈ b
15 1 2 3 4 infpssrlem4 ⊢ φ ∧ b ∈ ω ∧ c ∈ b → G ⁡ b ≠ G ⁡ c
16 12 13 14 15 syl3anc ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ c ∈ b → G ⁡ b ≠ G ⁡ c
17 11 16 jaodan ⊢ φ ∧ b ∈ ω ∧ c ∈ ω ∧ b ∈ c ∨ c ∈ b → G ⁡ b ≠ G ⁡ c
18 17 ex ⊢ φ ∧ b ∈ ω ∧ c ∈ ω → b ∈ c ∨ c ∈ b → G ⁡ b ≠ G ⁡ c
19 18 necon2bd ⊢ φ ∧ b ∈ ω ∧ c ∈ ω → G ⁡ b = G ⁡ c → ¬ b ∈ c ∨ c ∈ b
20 nnord ⊢ b ∈ ω → Ord ⁡ b
21 nnord ⊢ c ∈ ω → Ord ⁡ c
22 ordtri3 ⊢ Ord ⁡ b ∧ Ord ⁡ c → b = c ↔ ¬ b ∈ c ∨ c ∈ b
23 20 21 22 syl2an ⊢ b ∈ ω ∧ c ∈ ω → b = c ↔ ¬ b ∈ c ∨ c ∈ b
24 23 adantl ⊢ φ ∧ b ∈ ω ∧ c ∈ ω → b = c ↔ ¬ b ∈ c ∨ c ∈ b
25 19 24 sylibrd ⊢ φ ∧ b ∈ ω ∧ c ∈ ω → G ⁡ b = G ⁡ c → b = c
26 25 ralrimivva ⊢ φ → ∀ b ∈ ω ∀ c ∈ ω G ⁡ b = G ⁡ c → b = c
27 dff13 ⊢ G : ω ⟶ 1-1 A ↔ G : ω ⟶ A ∧ ∀ b ∈ ω ∀ c ∈ ω G ⁡ b = G ⁡ c → b = c
28 5 26 27 sylanbrc ⊢ φ → G : ω ⟶ 1-1 A
29 f1domg ⊢ A ∈ V → G : ω ⟶ 1-1 A → ω ≼ A
30 28 29 syl5com ⊢ φ → A ∈ V → ω ≼ A