This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ≼ 𝐵 → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )

Proof

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