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

Metamath Proof Explorer

Theorem nnadjuALT

Description: Shorter proof of nnadju using ax-rep . (Contributed by Paul Chapman, 11-Apr-2009) (Revised by Mario Carneiro, 6-Feb-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nnadjuALT 
|- ( ( A e. _om /\ B e. _om ) -> ( card ` ( A |_| B ) ) = ( A +o B ) )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( A e. _om -> A e. On )
2 nnon 
 |-  ( B e. _om -> B e. On )
3 onadju 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) ~~ ( A |_| B ) )
4 1 2 3 syl2an 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) ~~ ( A |_| B ) )
5 carden2b 
 |-  ( ( A +o B ) ~~ ( A |_| B ) -> ( card ` ( A +o B ) ) = ( card ` ( A |_| B ) ) )
6 4 5 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( card ` ( A +o B ) ) = ( card ` ( A |_| B ) ) )
7 nnacl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
8 cardnn 
 |-  ( ( A +o B ) e. _om -> ( card ` ( A +o B ) ) = ( A +o B ) )
9 7 8 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( card ` ( A +o B ) ) = ( A +o B ) )
10 6 9 eqtr3d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( card ` ( A |_| B ) ) = ( A +o B ) )