Step |
Hyp |
Ref |
Expression |
1 |
|
dfopg |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → 〈 𝐴 , 𝐵 〉 = { { 𝐴 } , { 𝐴 , 𝐵 } } ) |
2 |
|
snwf |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ) |
3 |
|
prwf |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) |
4 |
|
prwf |
⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ ∪ ( 𝑅1 “ On ) ) |
5 |
2 3 4
|
syl2an2r |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ ∪ ( 𝑅1 “ On ) ) |
6 |
1 5
|
eqeltrd |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → 〈 𝐴 , 𝐵 〉 ∈ ∪ ( 𝑅1 “ On ) ) |