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

Metamath Proof Explorer

Theorem opwf

Description: An ordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion opwf 
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 dfopg 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. = { { A } , { A , B } } )
2 snwf 
 |-  ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
3 prwf 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { A , B } e. U. ( R1 " On ) )
4 prwf 
 |-  ( ( { A } e. U. ( R1 " On ) /\ { A , B } e. U. ( R1 " On ) ) -> { { A } , { A , B } } e. U. ( R1 " On ) )
5 2 3 4 syl2an2r 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { { A } , { A , B } } e. U. ( R1 " On ) )
6 1 5 eqeltrd 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. e. U. ( R1 " On ) )