| Step |
Hyp |
Ref |
Expression |
| 1 |
|
wfax.1 |
⊢ 𝑊 = ∪ ( 𝑅1 “ On ) |
| 2 |
|
trwf |
⊢ Tr ∪ ( 𝑅1 “ On ) |
| 3 |
|
treq |
⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ( Tr 𝑊 ↔ Tr ∪ ( 𝑅1 “ On ) ) ) |
| 4 |
2 3
|
mpbiri |
⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → Tr 𝑊 ) |
| 5 |
|
vex |
⊢ 𝑓 ∈ V |
| 6 |
5
|
rnex |
⊢ ran 𝑓 ∈ V |
| 7 |
6
|
r1elss |
⊢ ( ran 𝑓 ∈ ∪ ( 𝑅1 “ On ) ↔ ran 𝑓 ⊆ ∪ ( 𝑅1 “ On ) ) |
| 8 |
7
|
biimpri |
⊢ ( ran 𝑓 ⊆ ∪ ( 𝑅1 “ On ) → ran 𝑓 ∈ ∪ ( 𝑅1 “ On ) ) |
| 9 |
1
|
sseq2i |
⊢ ( ran 𝑓 ⊆ 𝑊 ↔ ran 𝑓 ⊆ ∪ ( 𝑅1 “ On ) ) |
| 10 |
1
|
eleq2i |
⊢ ( ran 𝑓 ∈ 𝑊 ↔ ran 𝑓 ∈ ∪ ( 𝑅1 “ On ) ) |
| 11 |
8 9 10
|
3imtr4i |
⊢ ( ran 𝑓 ⊆ 𝑊 → ran 𝑓 ∈ 𝑊 ) |
| 12 |
11
|
3ad2ant3 |
⊢ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑊 ∧ ran 𝑓 ⊆ 𝑊 ) → ran 𝑓 ∈ 𝑊 ) |
| 13 |
12
|
ax-gen |
⊢ ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑊 ∧ ran 𝑓 ⊆ 𝑊 ) → ran 𝑓 ∈ 𝑊 ) |
| 14 |
13
|
a1i |
⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑊 ∧ ran 𝑓 ⊆ 𝑊 ) → ran 𝑓 ∈ 𝑊 ) ) |
| 15 |
|
onwf |
⊢ On ⊆ ∪ ( 𝑅1 “ On ) |
| 16 |
|
0elon |
⊢ ∅ ∈ On |
| 17 |
15 16
|
sselii |
⊢ ∅ ∈ ∪ ( 𝑅1 “ On ) |
| 18 |
|
eleq2 |
⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ( ∅ ∈ 𝑊 ↔ ∅ ∈ ∪ ( 𝑅1 “ On ) ) ) |
| 19 |
17 18
|
mpbiri |
⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ∅ ∈ 𝑊 ) |
| 20 |
4 14 19
|
modelaxrep |
⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
| 21 |
1 20
|
ax-mp |
⊢ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) |