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 e. Fin ) -> A ~<_ B )
2		simpr	|- ( ( A ~<_ B /\ A e. Fin ) -> A e. Fin )
3		reldom	|- Rel ~<_
4	3	brrelex2i	|- ( A ~<_ B -> B e. _V )
5	4	adantr	|- ( ( A ~<_ B /\ A e. Fin ) -> B e. _V )
6		hashdom	|- ( ( A e. Fin /\ B e. _V ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
7	2 5 6	syl2anc	|- ( ( A ~<_ B /\ A e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
8	1 7	mpbird	|- ( ( A ~<_ B /\ A e. Fin ) -> ( # ` A ) <_ ( # ` B ) )
9		pnfxr	|- +oo e. RR*
10		pnfge	|- ( +oo e. RR* -> +oo <_ +oo )
11	9 10	mp1i	|- ( ( A ~<_ B /\ -. A e. Fin ) -> +oo <_ +oo )
12	3	brrelex1i	|- ( A ~<_ B -> A e. _V )
13		hashinf	|- ( ( A e. _V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
14	12 13	sylan	|- ( ( A ~<_ B /\ -. A e. Fin ) -> ( # ` A ) = +oo )
15	4	adantr	|- ( ( A ~<_ B /\ -. A e. Fin ) -> B e. _V )
16		domfi	|- ( ( B e. Fin /\ A ~<_ B ) -> A e. Fin )
17	16	stoic1b	|- ( ( A ~<_ B /\ -. A e. Fin ) -> -. B e. Fin )
18		hashinf	|- ( ( B e. _V /\ -. B e. Fin ) -> ( # ` B ) = +oo )
19	15 17 18	syl2anc	|- ( ( A ~<_ B /\ -. A e. Fin ) -> ( # ` B ) = +oo )
20	11 14 19	3brtr4d	|- ( ( A ~<_ B /\ -. A e. Fin ) -> ( # ` A ) <_ ( # ` B ) )
21	8 20	pm2.61dan	|- ( A ~<_ B -> ( # ` A ) <_ ( # ` B ) )