Step |
Hyp |
Ref |
Expression |
1 |
|
r1elss.1 |
⊢ 𝐴 ∈ V |
2 |
|
r1elssi |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) |
3 |
1
|
tz9.12 |
⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
4 |
|
dfss3 |
⊢ ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) |
5 |
|
r1fnon |
⊢ 𝑅1 Fn On |
6 |
|
fnfun |
⊢ ( 𝑅1 Fn On → Fun 𝑅1 ) |
7 |
|
funiunfv |
⊢ ( Fun 𝑅1 → ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On ) ) |
8 |
5 6 7
|
mp2b |
⊢ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On ) |
9 |
8
|
eleq2i |
⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) |
10 |
|
eliun |
⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
11 |
9 10
|
bitr3i |
⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
12 |
11
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
13 |
4 12
|
bitri |
⊢ ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
14 |
8
|
eleq2i |
⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) |
15 |
|
eliun |
⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
16 |
14 15
|
bitr3i |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
17 |
3 13 16
|
3imtr4i |
⊢ ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) |
18 |
2 17
|
impbii |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) |