Step |
Hyp |
Ref |
Expression |
1 |
|
genp.1 |
⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } ) |
2 |
|
genp.2 |
⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q ) |
3 |
|
eqid |
⊢ ( 𝐶 𝐺 𝐷 ) = ( 𝐶 𝐺 𝐷 ) |
4 |
|
rspceov |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐶 𝐺 𝐷 ) = ( 𝐶 𝐺 𝐷 ) ) → ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ℎ ) ) |
5 |
3 4
|
mp3an3 |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ℎ ) ) |
6 |
1 2
|
genpelv |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ℎ ) ) ) |
7 |
5 6
|
syl5ibr |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ) ) |