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