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