Metamath Proof Explorer

Theorem prwf

Description: An unordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	prwf	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to \{A, B\} \in ⋃ R_{1} [On]$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
2		snwf	$⊢ A \in ⋃ R_{1} [On] \to \{A\} \in ⋃ R_{1} [On]$
3		snwf	$⊢ B \in ⋃ R_{1} [On] \to \{B\} \in ⋃ R_{1} [On]$
4		unwf	$⊢ (\{A\} \in ⋃ R_{1} [On] \land \{B\} \in ⋃ R_{1} [On]) \leftrightarrow \{A\} \cup \{B\} \in ⋃ R_{1} [On]$
5	4	biimpi	$⊢ (\{A\} \in ⋃ R_{1} [On] \land \{B\} \in ⋃ R_{1} [On]) \to \{A\} \cup \{B\} \in ⋃ R_{1} [On]$
6	2 3 5	syl2an	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to \{A\} \cup \{B\} \in ⋃ R_{1} [On]$
7	1 6	eqeltrid	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to \{A, B\} \in ⋃ R_{1} [On]$