Step |
Hyp |
Ref |
Expression |
1 |
|
eldm2g |
⊢ ( 𝐴 ∈ dom 𝐺 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 〈 𝐴 , 𝑦 〉 ∈ ( 𝐹 ∘ 𝐺 ) ) ) |
2 |
|
opelco2g |
⊢ ( ( 𝐴 ∈ dom 𝐺 ∧ 𝑦 ∈ V ) → ( 〈 𝐴 , 𝑦 〉 ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
3 |
2
|
elvd |
⊢ ( 𝐴 ∈ dom 𝐺 → ( 〈 𝐴 , 𝑦 〉 ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
4 |
3
|
exbidv |
⊢ ( 𝐴 ∈ dom 𝐺 → ( ∃ 𝑦 〈 𝐴 , 𝑦 〉 ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
5 |
1 4
|
bitrd |
⊢ ( 𝐴 ∈ dom 𝐺 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
6 |
5
|
adantl |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
7 |
|
fvex |
⊢ ( 𝐺 ‘ 𝐴 ) ∈ V |
8 |
7
|
eldm2 |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦 〈 ( 𝐺 ‘ 𝐴 ) , 𝑦 〉 ∈ 𝐹 ) |
9 |
|
opeq1 |
⊢ ( 𝑥 = ( 𝐺 ‘ 𝐴 ) → 〈 𝑥 , 𝑦 〉 = 〈 ( 𝐺 ‘ 𝐴 ) , 𝑦 〉 ) |
10 |
9
|
eleq1d |
⊢ ( 𝑥 = ( 𝐺 ‘ 𝐴 ) → ( 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ↔ 〈 ( 𝐺 ‘ 𝐴 ) , 𝑦 〉 ∈ 𝐹 ) ) |
11 |
7 10
|
ceqsexv |
⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ↔ 〈 ( 𝐺 ‘ 𝐴 ) , 𝑦 〉 ∈ 𝐹 ) |
12 |
|
eqcom |
⊢ ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ↔ ( 𝐺 ‘ 𝐴 ) = 𝑥 ) |
13 |
|
funopfvb |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐺 ‘ 𝐴 ) = 𝑥 ↔ 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ) ) |
14 |
12 13
|
syl5bb |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ↔ 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ) ) |
15 |
14
|
anbi1d |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ↔ ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
16 |
15
|
exbidv |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ∃ 𝑥 ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ↔ ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
17 |
11 16
|
bitr3id |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 〈 ( 𝐺 ‘ 𝐴 ) , 𝑦 〉 ∈ 𝐹 ↔ ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
18 |
17
|
exbidv |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ∃ 𝑦 〈 ( 𝐺 ‘ 𝐴 ) , 𝑦 〉 ∈ 𝐹 ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
19 |
8 18
|
syl5bb |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐺 ‘ 𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝐴 , 𝑥 〉 ∈ 𝐺 ∧ 〈 𝑥 , 𝑦 〉 ∈ 𝐹 ) ) ) |
20 |
6 19
|
bitr4d |
⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐺 ‘ 𝐴 ) ∈ dom 𝐹 ) ) |