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 ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B ∈ ⋃ R1 On

Proof

Step Hyp Ref Expression
1 dfopg ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B = A A B
2 snwf ⊢ A ∈ ⋃ R1 On → A ∈ ⋃ R1 On
3 prwf ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B ∈ ⋃ R1 On
4 prwf ⊢ A ∈ ⋃ R1 On ∧ A B ∈ ⋃ R1 On → A A B ∈ ⋃ R1 On
5 2 3 4 syl2an2r ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A A B ∈ ⋃ R1 On
6 1 5 eqeltrd ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B ∈ ⋃ R1 On