Step | Hyp | Ref
| Expression |
1 | | prop 6458 |
. . . . . . . . 9
⊢ (A ∈
P → ⟨(1^{st} ‘A), (2^{nd} ‘A)⟩ ∈
P) |
2 | | elprnqu 6465 |
. . . . . . . . 9
⊢
((⟨(1^{st} ‘A),
(2^{nd} ‘A)⟩ ∈ P ∧ f ∈ (2^{nd} ‘A)) → f
∈ Q) |
3 | 1, 2 | sylan 267 |
. . . . . . . 8
⊢
((A ∈ P ∧ f ∈ (2^{nd} ‘A)) → f
∈ Q) |
4 | | prop 6458 |
. . . . . . . . . . . . . . . 16
⊢ (B ∈
P → ⟨(1^{st} ‘B), (2^{nd} ‘B)⟩ ∈
P) |
5 | | elprnqu 6465 |
. . . . . . . . . . . . . . . 16
⊢
((⟨(1^{st} ‘B),
(2^{nd} ‘B)⟩ ∈ P ∧ g ∈ (2^{nd} ‘B)) → g
∈ Q) |
6 | 4, 5 | sylan 267 |
. . . . . . . . . . . . . . 15
⊢
((B ∈ P ∧ g ∈ (2^{nd} ‘B)) → g
∈ Q) |
7 | | r19.41v 2460 |
. . . . . . . . . . . . . . . . 17
⊢ (∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))) |
8 | | prop 6458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 ∈ P → ⟨(1^{st}
‘𝐶), (2^{nd}
‘𝐶)⟩ ∈ P) |
9 | | elprnqu 6465 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⟨(1^{st} ‘𝐶), (2^{nd} ‘𝐶)⟩ ∈
P ∧ ℎ ∈
(2^{nd} ‘𝐶))
→ ℎ ∈ Q) |
10 | 8, 9 | sylan 267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 ∈ P ∧ ℎ
∈ (2^{nd} ‘𝐶)) → ℎ ∈
Q) |
11 | | oveq2 5463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = (g𝐺ℎ) → (f𝐺𝑡) = (f𝐺(g𝐺ℎ))) |
12 | 11 | adantr 261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q)) → (f𝐺𝑡) = (f𝐺(g𝐺ℎ))) |
13 | | genpassg.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ))) |
14 | 13 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q)) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ))) |
15 | 12, 14 | eqtr4d 2072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q)) → (f𝐺𝑡) = ((f𝐺g)𝐺ℎ)) |
16 | 15 | eqeq2d 2048 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q)) → (x = (f𝐺𝑡) ↔ x = ((f𝐺g)𝐺ℎ))) |
17 | 16 | expcom 109 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → (𝑡 = (g𝐺ℎ) → (x = (f𝐺𝑡) ↔ x = ((f𝐺g)𝐺ℎ)))) |
18 | 17 | pm5.32d 423 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
19 | 18 | 3expa 1103 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((f ∈ Q ∧ g ∈ Q) ∧ ℎ
∈ Q) → ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
20 | 10, 19 | sylan2 270 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((f ∈ Q ∧ g ∈ Q) ∧ (𝐶 ∈
P ∧ ℎ ∈
(2^{nd} ‘𝐶)))
→ ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
21 | 20 | anassrs 380 |
. . . . . . . . . . . . . . . . . 18
⊢
((((f ∈ Q ∧ g ∈ Q) ∧ 𝐶 ∈
P) ∧ ℎ ∈
(2^{nd} ‘𝐶))
→ ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
22 | 21 | rexbidva 2317 |
. . . . . . . . . . . . . . . . 17
⊢
(((f ∈ Q ∧ g ∈ Q) ∧ 𝐶 ∈
P) → (∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ ∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
23 | 7, 22 | syl5rbbr 184 |
. . . . . . . . . . . . . . . 16
⊢
(((f ∈ Q ∧ g ∈ Q) ∧ 𝐶 ∈
P) → (∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
24 | 23 | an32s 502 |
. . . . . . . . . . . . . . 15
⊢
(((f ∈ Q ∧ 𝐶 ∈
P) ∧ g ∈
Q) → (∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
25 | 6, 24 | sylan2 270 |
. . . . . . . . . . . . . 14
⊢
(((f ∈ Q ∧ 𝐶 ∈
P) ∧ (B ∈
P ∧ g ∈
(2^{nd} ‘B))) → (∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
26 | 25 | anassrs 380 |
. . . . . . . . . . . . 13
⊢
((((f ∈ Q ∧ 𝐶 ∈
P) ∧ B ∈
P) ∧ g ∈
(2^{nd} ‘B)) → (∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
27 | 26 | rexbidva 2317 |
. . . . . . . . . . . 12
⊢
(((f ∈ Q ∧ 𝐶 ∈
P) ∧ B ∈
P) → (∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃g ∈ (2^{nd} ‘B)(∃ℎ ∈
(2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
28 | | r19.41v 2460 |
. . . . . . . . . . . 12
⊢ (∃g ∈ (2^{nd} ‘B)(∃ℎ ∈
(2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))) |
29 | 27, 28 | syl6bb 185 |
. . . . . . . . . . 11
⊢
(((f ∈ Q ∧ 𝐶 ∈
P) ∧ B ∈
P) → (∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
30 | 29 | an31s 504 |
. . . . . . . . . 10
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ f ∈
Q) → (∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
31 | 30 | exbidv 1703 |
. . . . . . . . 9
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ f ∈
Q) → (∃𝑡∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃𝑡(∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
32 | | genpelvl.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q) |
33 | 32 | caovcl 5597 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g𝐺ℎ) ∈
Q) |
34 | | elisset 2562 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((g𝐺ℎ) ∈
Q → ∃𝑡 𝑡 = (g𝐺ℎ)) |
35 | 33, 34 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((g ∈ Q ∧ ℎ
∈ Q) → ∃𝑡 𝑡 = (g𝐺ℎ)) |
36 | 35 | biantrurd 289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (x = ((f𝐺g)𝐺ℎ) ↔ (∃𝑡 𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
37 | | 19.41v 1779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))) |
38 | 36, 37 | syl6bbr 187 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
39 | 10, 38 | sylan2 270 |
. . . . . . . . . . . . . . . . . . 19
⊢
((g ∈ Q ∧ (𝐶 ∈
P ∧ ℎ ∈
(2^{nd} ‘𝐶)))
→ (x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
40 | 39 | anassrs 380 |
. . . . . . . . . . . . . . . . . 18
⊢
(((g ∈ Q ∧ 𝐶 ∈
P) ∧ ℎ ∈
(2^{nd} ‘𝐶))
→ (x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
41 | 40 | rexbidva 2317 |
. . . . . . . . . . . . . . . . 17
⊢
((g ∈ Q ∧ 𝐶 ∈
P) → (∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃ℎ
∈ (2^{nd} ‘𝐶)∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
42 | | rexcom4 2571 |
. . . . . . . . . . . . . . . . 17
⊢ (∃ℎ
∈ (2^{nd} ‘𝐶)∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃𝑡∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))) |
43 | 41, 42 | syl6bb 185 |
. . . . . . . . . . . . . . . 16
⊢
((g ∈ Q ∧ 𝐶 ∈
P) → (∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
44 | 43 | ancoms 255 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ P ∧ g ∈ Q) → (∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
45 | 6, 44 | sylan2 270 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ P ∧ (B ∈ P ∧ g ∈ (2^{nd} ‘B))) → (∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
46 | 45 | anassrs 380 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ P ∧ B ∈ P) ∧ g ∈ (2^{nd} ‘B)) → (∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈
(2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
47 | 46 | rexbidva 2317 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ P ∧ B ∈ P) → (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃g ∈ (2^{nd} ‘B)∃𝑡∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
48 | 47 | ancoms 255 |
. . . . . . . . . . 11
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃g ∈ (2^{nd} ‘B)∃𝑡∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
49 | | rexcom4 2571 |
. . . . . . . . . . 11
⊢ (∃g ∈ (2^{nd} ‘B)∃𝑡∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))) |
50 | 48, 49 | syl6bb 185 |
. . . . . . . . . 10
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
51 | 50 | adantr 261 |
. . . . . . . . 9
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ f ∈
Q) → (∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))) |
52 | | df-rex 2306 |
. . . . . . . . . . 11
⊢ (∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃𝑡(𝑡 ∈
(2^{nd} ‘(B𝐹𝐶)) ∧
x = (f𝐺𝑡))) |
53 | | genpelvl.1 |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (w ∈
P, v ∈ P ↦ ⟨{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (1^{st} ‘w) ∧ z ∈
(1^{st} ‘v) ∧ x = (y𝐺z))},
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2^{nd} ‘w) ∧ z ∈
(2^{nd} ‘v) ∧ x = (y𝐺z))}⟩) |
54 | 53, 32 | genpelvu 6496 |
. . . . . . . . . . . . 13
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (𝑡
∈ (2^{nd} ‘(B𝐹𝐶)) ↔ ∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ))) |
55 | 54 | anbi1d 438 |
. . . . . . . . . . . 12
⊢
((B ∈ P ∧ 𝐶 ∈
P) → ((𝑡
∈ (2^{nd} ‘(B𝐹𝐶)) ∧
x = (f𝐺𝑡)) ↔ (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
56 | 55 | exbidv 1703 |
. . . . . . . . . . 11
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (∃𝑡(𝑡 ∈
(2^{nd} ‘(B𝐹𝐶)) ∧
x = (f𝐺𝑡)) ↔ ∃𝑡(∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
57 | 52, 56 | syl5bb 181 |
. . . . . . . . . 10
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃𝑡(∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
58 | 57 | adantr 261 |
. . . . . . . . 9
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ f ∈
Q) → (∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃𝑡(∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))) |
59 | 31, 51, 58 | 3bitr4rd 210 |
. . . . . . . 8
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ f ∈
Q) → (∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
60 | 3, 59 | sylan2 270 |
. . . . . . 7
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ (A ∈
P ∧ f ∈
(2^{nd} ‘A))) → (∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
61 | 60 | anassrs 380 |
. . . . . 6
⊢
((((B ∈ P ∧ 𝐶 ∈
P) ∧ A ∈
P) ∧ f ∈
(2^{nd} ‘A)) → (∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
62 | 61 | rexbidva 2317 |
. . . . 5
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ A ∈
P) → (∃f ∈
(2^{nd} ‘A)∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
63 | 62 | ancoms 255 |
. . . 4
⊢
((A ∈ P ∧ (B ∈ P ∧ 𝐶 ∈
P)) → (∃f ∈
(2^{nd} ‘A)∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
64 | 63 | 3impb 1099 |
. . 3
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (∃f ∈
(2^{nd} ‘A)∃𝑡 ∈
(2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡) ↔ ∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
65 | | genpassg.5 |
. . . . . 6
⊢
((f ∈ P ∧ g ∈ P) → (f𝐹g) ∈ P) |
66 | 65 | caovcl 5597 |
. . . . 5
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (B𝐹𝐶) ∈
P) |
67 | 53, 32 | genpelvu 6496 |
. . . . 5
⊢
((A ∈ P ∧ (B𝐹𝐶) ∈
P) → (x ∈ (2^{nd} ‘(A𝐹(B𝐹𝐶))) ↔ ∃f ∈ (2^{nd} ‘A)∃𝑡 ∈ (2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡))) |
68 | 66, 67 | sylan2 270 |
. . . 4
⊢
((A ∈ P ∧ (B ∈ P ∧ 𝐶 ∈
P)) → (x ∈ (2^{nd} ‘(A𝐹(B𝐹𝐶))) ↔ ∃f ∈ (2^{nd} ‘A)∃𝑡 ∈ (2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡))) |
69 | 68 | 3impb 1099 |
. . 3
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (x ∈ (2^{nd} ‘(A𝐹(B𝐹𝐶))) ↔ ∃f ∈ (2^{nd} ‘A)∃𝑡 ∈ (2^{nd} ‘(B𝐹𝐶))x =
(f𝐺𝑡))) |
70 | | df-rex 2306 |
. . . . 5
⊢ (∃𝑡 ∈
(2^{nd} ‘(A𝐹B))∃ℎ
∈ (2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ) ↔ ∃𝑡(𝑡 ∈
(2^{nd} ‘(A𝐹B))
∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
71 | 53, 32 | genpelvu 6496 |
. . . . . . . 8
⊢
((A ∈ P ∧ B ∈ P) → (𝑡 ∈
(2^{nd} ‘(A𝐹B))
↔ ∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g))) |
72 | 71 | 3adant3 923 |
. . . . . . 7
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (𝑡
∈ (2^{nd} ‘(A𝐹B))
↔ ∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g))) |
73 | 72 | anbi1d 438 |
. . . . . 6
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → ((𝑡
∈ (2^{nd} ‘(A𝐹B))
∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
74 | 73 | exbidv 1703 |
. . . . 5
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (∃𝑡(𝑡 ∈
(2^{nd} ‘(A𝐹B))
∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ ∃𝑡(∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
75 | 70, 74 | syl5bb 181 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (∃𝑡 ∈
(2^{nd} ‘(A𝐹B))∃ℎ
∈ (2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ) ↔ ∃𝑡(∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
76 | 65 | caovcl 5597 |
. . . . . 6
⊢
((A ∈ P ∧ B ∈ P) → (A𝐹B) ∈ P) |
77 | 53, 32 | genpelvu 6496 |
. . . . . 6
⊢
(((A𝐹B) ∈ P ∧ 𝐶 ∈
P) → (x ∈ (2^{nd} ‘((A𝐹B)𝐹𝐶)) ↔ ∃𝑡 ∈
(2^{nd} ‘(A𝐹B))∃ℎ
∈ (2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
78 | 76, 77 | sylan 267 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P) ∧ 𝐶 ∈
P) → (x ∈ (2^{nd} ‘((A𝐹B)𝐹𝐶)) ↔ ∃𝑡 ∈
(2^{nd} ‘(A𝐹B))∃ℎ
∈ (2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
79 | 78 | 3impa 1098 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (x ∈ (2^{nd} ‘((A𝐹B)𝐹𝐶)) ↔ ∃𝑡 ∈
(2^{nd} ‘(A𝐹B))∃ℎ
∈ (2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
80 | 32 | caovcl 5597 |
. . . . . . . . . . . . . . . . . . 19
⊢
((f ∈ Q ∧ g ∈ Q) → (f𝐺g) ∈ Q) |
81 | | elisset 2562 |
. . . . . . . . . . . . . . . . . . 19
⊢
((f𝐺g) ∈ Q → ∃𝑡 𝑡 = (f𝐺g)) |
82 | 80, 81 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢
((f ∈ Q ∧ g ∈ Q) → ∃𝑡 𝑡 = (f𝐺g)) |
83 | 82 | biantrurd 289 |
. . . . . . . . . . . . . . . . 17
⊢
((f ∈ Q ∧ g ∈ Q) → (∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ (∃𝑡 𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ)))) |
84 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = (f𝐺g)
→ (𝑡𝐺ℎ) = ((f𝐺g)𝐺ℎ)) |
85 | 84 | eqeq2d 2048 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (f𝐺g)
→ (x = (𝑡𝐺ℎ) ↔ x
= ((f𝐺g)𝐺ℎ))) |
86 | 85 | rexbidv 2321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (f𝐺g)
→ (∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ) ↔ ∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
87 | 86 | pm5.32i 427 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ (𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
88 | 87 | exbii 1493 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
89 | | 19.41v 1779 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
90 | 88, 89 | bitri 173 |
. . . . . . . . . . . . . . . . 17
⊢ (∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ (∃𝑡 𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
91 | 83, 90 | syl6bbr 187 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ Q ∧ g ∈ Q) → (∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
92 | 6, 91 | sylan2 270 |
. . . . . . . . . . . . . . 15
⊢
((f ∈ Q ∧ (B ∈ P ∧ g ∈ (2^{nd} ‘B))) → (∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
93 | 92 | anassrs 380 |
. . . . . . . . . . . . . 14
⊢
(((f ∈ Q ∧ B ∈ P) ∧ g ∈ (2^{nd} ‘B)) → (∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
94 | 93 | rexbidva 2317 |
. . . . . . . . . . . . 13
⊢
((f ∈ Q ∧ B ∈ P) → (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃g ∈ (2^{nd} ‘B)∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
95 | | rexcom4 2571 |
. . . . . . . . . . . . 13
⊢ (∃g ∈ (2^{nd} ‘B)∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
96 | 94, 95 | syl6bb 185 |
. . . . . . . . . . . 12
⊢
((f ∈ Q ∧ B ∈ P) → (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
97 | 96 | ancoms 255 |
. . . . . . . . . . 11
⊢
((B ∈ P ∧ f ∈ Q) → (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
98 | 3, 97 | sylan2 270 |
. . . . . . . . . 10
⊢
((B ∈ P ∧ (A ∈ P ∧ f ∈ (2^{nd} ‘A))) → (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
99 | 98 | anassrs 380 |
. . . . . . . . 9
⊢
(((B ∈ P ∧ A ∈ P) ∧ f ∈ (2^{nd} ‘A)) → (∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈
(2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
100 | 99 | rexbidva 2317 |
. . . . . . . 8
⊢
((B ∈ P ∧ A ∈ P) → (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃f ∈ (2^{nd} ‘A)∃𝑡∃g ∈ (2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
101 | | rexcom4 2571 |
. . . . . . . 8
⊢ (∃f ∈ (2^{nd} ‘A)∃𝑡∃g ∈ (2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ ∃𝑡∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
102 | 100, 101 | syl6bb 185 |
. . . . . . 7
⊢
((B ∈ P ∧ A ∈ P) → (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
103 | | r19.41v 2460 |
. . . . . . . . . 10
⊢ (∃g ∈ (2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ (∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
104 | 103 | rexbii 2325 |
. . . . . . . . 9
⊢ (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ ∃f ∈ (2^{nd} ‘A)(∃g ∈
(2^{nd} ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
105 | | r19.41v 2460 |
. . . . . . . . 9
⊢ (∃f ∈ (2^{nd} ‘A)(∃g ∈
(2^{nd} ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
106 | 104, 105 | bitri 173 |
. . . . . . . 8
⊢ (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
107 | 106 | exbii 1493 |
. . . . . . 7
⊢ (∃𝑡∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)) ↔ ∃𝑡(∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ))) |
108 | 102, 107 | syl6bb 185 |
. . . . . 6
⊢
((B ∈ P ∧ A ∈ P) → (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡(∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
109 | 108 | ancoms 255 |
. . . . 5
⊢
((A ∈ P ∧ B ∈ P) → (∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡(∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
110 | 109 | 3adant3 923 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)∃ℎ ∈
(2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ) ↔ ∃𝑡(∃f ∈
(2^{nd} ‘A)∃g ∈ (2^{nd} ‘B)𝑡
= (f𝐺g) ∧ ∃ℎ ∈
(2^{nd} ‘𝐶)x =
(𝑡𝐺ℎ)))) |
111 | 75, 79, 110 | 3bitr4d 209 |
. . 3
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (x ∈ (2^{nd} ‘((A𝐹B)𝐹𝐶)) ↔ ∃f ∈ (2^{nd} ‘A)∃g ∈
(2^{nd} ‘B)∃ℎ
∈ (2^{nd} ‘𝐶)x =
((f𝐺g)𝐺ℎ))) |
112 | 64, 69, 111 | 3bitr4rd 210 |
. 2
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (x ∈ (2^{nd} ‘((A𝐹B)𝐹𝐶)) ↔ x ∈
(2^{nd} ‘(A𝐹(B𝐹𝐶))))) |
113 | 112 | eqrdv 2035 |
1
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (2^{nd} ‘((A𝐹B)𝐹𝐶)) = (2^{nd} ‘(A𝐹(B𝐹𝐶)))) |