opwf

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

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

Step	Hyp	Ref	Expression
1		dfopg	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
2		snwf	$⊢ A \in ⋃ R_{1} [On] \to \{A\} \in ⋃ R_{1} [On]$
3		prwf	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to \{A, B\} \in ⋃ R_{1} [On]$
4		prwf	$⊢ (\{A\} \in ⋃ R_{1} [On] \land \{A, B\} \in ⋃ R_{1} [On]) \to \{\{A\}, \{A, B\}\} \in ⋃ R_{1} [On]$
5	2 3 4	syl2an2r	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to \{\{A\}, \{A, B\}\} \in ⋃ R_{1} [On]$
6	1 5	eqeltrd	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to ⟨A, B⟩ \in ⋃ R_{1} [On]$

Metamath Proof Explorer