Description: An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004) (Revised by Mario Carneiro, 27-Apr-2015) Avoid ax-pow . (Revised by BTernaryTau, 7-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | infsdomnn | ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ∈ ω ) → 𝐵 ≺ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnfi | ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ Fin ) | |
| 2 | 1 | adantl | ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ∈ ω ) → 𝐵 ∈ Fin ) |
| 3 | reldom | ⊢ Rel ≼ | |
| 4 | 3 | brrelex1i | ⊢ ( ω ≼ 𝐴 → ω ∈ V ) |
| 5 | nnsdomg | ⊢ ( ( ω ∈ V ∧ 𝐵 ∈ ω ) → 𝐵 ≺ ω ) | |
| 6 | 4 5 | sylan | ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ∈ ω ) → 𝐵 ≺ ω ) |
| 7 | simpl | ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ∈ ω ) → ω ≼ 𝐴 ) | |
| 8 | sdomdomtrfi | ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐵 ≺ ω ∧ ω ≼ 𝐴 ) → 𝐵 ≺ 𝐴 ) | |
| 9 | 2 6 7 8 | syl3anc | ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ∈ ω ) → 𝐵 ≺ 𝐴 ) |