Step |
Hyp |
Ref |
Expression |
1 |
|
19.8a |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) |
2 |
1
|
ancoms |
⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) |
3 |
|
vex |
⊢ 𝑦 ∈ V |
4 |
3
|
elima2 |
⊢ ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) |
5 |
2 4
|
sylibr |
⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ( 𝑅 “ 𝐴 ) ) |
6 |
|
simpl |
⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 𝑅 𝑦 ) |
7 |
|
vex |
⊢ 𝑥 ∈ V |
8 |
3 7
|
brcnv |
⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) |
9 |
6 8
|
sylibr |
⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ◡ 𝑅 𝑥 ) |
10 |
5 9
|
jca |
⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) ) |
11 |
10
|
eximi |
⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) ) |
12 |
7
|
eldm |
⊢ ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 ) |
13 |
12
|
anbi1i |
⊢ ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) ) |
14 |
|
elin |
⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ 𝐴 ) ) |
15 |
|
19.41v |
⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) ) |
16 |
13 14 15
|
3bitr4i |
⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑥 ∈ 𝐴 ) ) |
17 |
7
|
elima2 |
⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ◡ 𝑅 𝑥 ) ) |
18 |
11 16 17
|
3imtr4i |
⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) → 𝑥 ∈ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) ) ) |
19 |
18
|
ssriv |
⊢ ( dom 𝑅 ∩ 𝐴 ) ⊆ ( ◡ 𝑅 “ ( 𝑅 “ 𝐴 ) ) |