Metamath Proof Explorer

Theorem hashdomi

Description: Non-strict order relation of the # function on the full cardinal poset. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion hashdomi ⊢ A ≼ B → A ≤ B

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ≼ B ∧ A ∈ Fin → A ≼ B
2 simpr ⊢ A ≼ B ∧ A ∈ Fin → A ∈ Fin
3 reldom ⊢ Rel ⁡ ≼
4 3 brrelex2i ⊢ A ≼ B → B ∈ V
5 4 adantr ⊢ A ≼ B ∧ A ∈ Fin → B ∈ V
6 hashdom ⊢ A ∈ Fin ∧ B ∈ V → A ≤ B ↔ A ≼ B
7 2 5 6 syl2anc ⊢ A ≼ B ∧ A ∈ Fin → A ≤ B ↔ A ≼ B
8 1 7 mpbird ⊢ A ≼ B ∧ A ∈ Fin → A ≤ B
9 pnfxr ⊢ +∞ ∈ ℝ *
10 pnfge ⊢ +∞ ∈ ℝ * → +∞ ≤ +∞
11 9 10 mp1i ⊢ A ≼ B ∧ ¬ A ∈ Fin → +∞ ≤ +∞
12 3 brrelex1i ⊢ A ≼ B → A ∈ V
13 hashinf ⊢ A ∈ V ∧ ¬ A ∈ Fin → A = +∞
14 12 13 sylan ⊢ A ≼ B ∧ ¬ A ∈ Fin → A = +∞
15 4 adantr ⊢ A ≼ B ∧ ¬ A ∈ Fin → B ∈ V
16 domfi ⊢ B ∈ Fin ∧ A ≼ B → A ∈ Fin
17 16 stoic1b ⊢ A ≼ B ∧ ¬ A ∈ Fin → ¬ B ∈ Fin
18 hashinf ⊢ B ∈ V ∧ ¬ B ∈ Fin → B = +∞
19 15 17 18 syl2anc ⊢ A ≼ B ∧ ¬ A ∈ Fin → B = +∞
20 11 14 19 3brtr4d ⊢ A ≼ B ∧ ¬ A ∈ Fin → A ≤ B
21 8 20 pm2.61dan ⊢ A ≼ B → A ≤ B