Step | Hyp | Ref
| Expression |
1 | | prop 6458 |
. . . 4
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
2 | | prmu 6461 |
. . . 4
⊢
(〈(1st ‘A),
(2nd ‘A)〉 ∈ P → ∃f ∈ Q f ∈
(2nd ‘A)) |
3 | | rexex 2362 |
. . . 4
⊢ (∃f ∈ Q f ∈
(2nd ‘A) → ∃f f ∈
(2nd ‘A)) |
4 | 1, 2, 3 | 3syl 17 |
. . 3
⊢ (A ∈
P → ∃f f ∈ (2nd ‘A)) |
5 | 4 | adantr 261 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → ∃f f ∈
(2nd ‘A)) |
6 | | prop 6458 |
. . . . 5
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
7 | | prmu 6461 |
. . . . 5
⊢
(〈(1st ‘B),
(2nd ‘B)〉 ∈ P → ∃g ∈ Q g ∈
(2nd ‘B)) |
8 | | rexex 2362 |
. . . . 5
⊢ (∃g ∈ Q g ∈
(2nd ‘B) → ∃g g ∈
(2nd ‘B)) |
9 | 6, 7, 8 | 3syl 17 |
. . . 4
⊢ (B ∈
P → ∃g g ∈ (2nd ‘B)) |
10 | 9 | ad2antlr 458 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P) ∧ f ∈ (2nd ‘A)) → ∃g g ∈
(2nd ‘B)) |
11 | | genpelvl.1 |
. . . . . . 7
⊢ 𝐹 = (w ∈
P, v ∈ P ↦ 〈{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1st ‘w) ∧ z ∈
(1st ‘v) ∧ x = (y𝐺z))},
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘w) ∧ z ∈
(2nd ‘v) ∧ x = (y𝐺z))}〉) |
12 | | genpelvl.2 |
. . . . . . 7
⊢
((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q) |
13 | 11, 12 | genppreclu 6498 |
. . . . . 6
⊢
((A ∈ P ∧ B ∈ P) → ((f ∈
(2nd ‘A) ∧ g ∈ (2nd ‘B)) → (f𝐺g) ∈ (2nd ‘(A𝐹B)))) |
14 | 13 | imp 115 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P) ∧ (f ∈ (2nd ‘A) ∧ g ∈
(2nd ‘B))) →
(f𝐺g) ∈ (2nd ‘(A𝐹B))) |
15 | | elprnqu 6465 |
. . . . . . . . . 10
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ f ∈ (2nd ‘A)) → f
∈ Q) |
16 | 1, 15 | sylan 267 |
. . . . . . . . 9
⊢
((A ∈ P ∧ f ∈ (2nd ‘A)) → f
∈ Q) |
17 | | elprnqu 6465 |
. . . . . . . . . 10
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ g ∈ (2nd ‘B)) → g
∈ Q) |
18 | 6, 17 | sylan 267 |
. . . . . . . . 9
⊢
((B ∈ P ∧ g ∈ (2nd ‘B)) → g
∈ Q) |
19 | 16, 18 | anim12i 321 |
. . . . . . . 8
⊢
(((A ∈ P ∧ f ∈ (2nd ‘A)) ∧ (B ∈
P ∧ g ∈
(2nd ‘B))) →
(f ∈
Q ∧ g ∈
Q)) |
20 | 19 | an4s 522 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P) ∧ (f ∈ (2nd ‘A) ∧ g ∈
(2nd ‘B))) →
(f ∈
Q ∧ g ∈
Q)) |
21 | 12 | caovcl 5597 |
. . . . . . 7
⊢
((f ∈ Q ∧ g ∈ Q) → (f𝐺g) ∈ Q) |
22 | 20, 21 | syl 14 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P) ∧ (f ∈ (2nd ‘A) ∧ g ∈
(2nd ‘B))) →
(f𝐺g) ∈ Q) |
23 | | simpr 103 |
. . . . . . 7
⊢
((((A ∈ P ∧ B ∈ P) ∧ (f ∈ (2nd ‘A) ∧ g ∈
(2nd ‘B))) ∧ 𝑞
= (f𝐺g))
→ 𝑞 = (f𝐺g)) |
24 | 23 | eleq1d 2103 |
. . . . . 6
⊢
((((A ∈ P ∧ B ∈ P) ∧ (f ∈ (2nd ‘A) ∧ g ∈
(2nd ‘B))) ∧ 𝑞
= (f𝐺g))
→ (𝑞 ∈ (2nd ‘(A𝐹B))
↔ (f𝐺g) ∈ (2nd ‘(A𝐹B)))) |
25 | 22, 24 | rspcedv 2654 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P) ∧ (f ∈ (2nd ‘A) ∧ g ∈
(2nd ‘B))) →
((f𝐺g) ∈ (2nd ‘(A𝐹B))
→ ∃𝑞 ∈
Q 𝑞 ∈ (2nd ‘(A𝐹B)))) |
26 | 14, 25 | mpd 13 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P) ∧ (f ∈ (2nd ‘A) ∧ g ∈
(2nd ‘B))) → ∃𝑞 ∈
Q 𝑞 ∈ (2nd ‘(A𝐹B))) |
27 | 26 | anassrs 380 |
. . 3
⊢
((((A ∈ P ∧ B ∈ P) ∧ f ∈ (2nd ‘A)) ∧ g ∈
(2nd ‘B)) → ∃𝑞 ∈
Q 𝑞 ∈ (2nd ‘(A𝐹B))) |
28 | 10, 27 | exlimddv 1775 |
. 2
⊢
(((A ∈ P ∧ B ∈ P) ∧ f ∈ (2nd ‘A)) → ∃𝑞 ∈ Q 𝑞 ∈
(2nd ‘(A𝐹B))) |
29 | 5, 28 | exlimddv 1775 |
1
⊢
((A ∈ P ∧ B ∈ P) → ∃𝑞 ∈
Q 𝑞 ∈ (2nd ‘(A𝐹B))) |