Step |
Hyp |
Ref |
Expression |
1 |
|
wfax.1 |
⊢ 𝑊 = ∪ ( 𝑅1 “ On ) |
2 |
|
prwf |
⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) ) |
3 |
1
|
eleq2i |
⊢ ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) |
4 |
1
|
eleq2i |
⊢ ( 𝑦 ∈ 𝑊 ↔ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) |
5 |
3 4
|
anbi12i |
⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ↔ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ) |
6 |
1
|
eleq2i |
⊢ ( { 𝑥 , 𝑦 } ∈ 𝑊 ↔ { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) ) |
7 |
2 5 6
|
3imtr4i |
⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → { 𝑥 , 𝑦 } ∈ 𝑊 ) |
8 |
7
|
rgen2 |
⊢ ∀ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 { 𝑥 , 𝑦 } ∈ 𝑊 |
9 |
|
prclaxpr |
⊢ ( ∀ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 { 𝑥 , 𝑦 } ∈ 𝑊 → ∀ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 ∃ 𝑧 ∈ 𝑊 ∀ 𝑤 ∈ 𝑊 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) |
10 |
8 9
|
ax-mp |
⊢ ∀ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 ∃ 𝑧 ∈ 𝑊 ∀ 𝑤 ∈ 𝑊 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) |