Step | Hyp | Ref
| Expression |
1 | | prop 7424 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
2 | | elprnql 7430 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑓 ∈ (1st
‘𝐴)) → 𝑓 ∈
Q) |
3 | 1, 2 | sylan 281 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (1st
‘𝐴)) → 𝑓 ∈
Q) |
4 | | prop 7424 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
5 | | elprnql 7430 |
. . . . . . . . . . . . . . . 16
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑔 ∈ (1st
‘𝐵)) → 𝑔 ∈
Q) |
6 | 4, 5 | sylan 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ P ∧
𝑔 ∈ (1st
‘𝐵)) → 𝑔 ∈
Q) |
7 | | prop 7424 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 ∈ P →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
8 | | elprnql 7430 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ P ∧ ℎ ∈ (1st
‘𝐶)) → ℎ ∈
Q) |
9 | 7, 8 | sylan 281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 ∈ P ∧
ℎ ∈ (1st
‘𝐶)) → ℎ ∈
Q) |
10 | | oveq2 5858 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = (𝑔𝐺ℎ) → (𝑓𝐺𝑡) = (𝑓𝐺(𝑔𝐺ℎ))) |
11 | 10 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧
ℎ ∈ Q))
→ (𝑓𝐺𝑡) = (𝑓𝐺(𝑔𝐺ℎ))) |
12 | | genpassg.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) |
13 | 12 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧
ℎ ∈ Q))
→ ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) |
14 | 11, 13 | eqtr4d 2206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧
ℎ ∈ Q))
→ (𝑓𝐺𝑡) = ((𝑓𝐺𝑔)𝐺ℎ)) |
15 | 14 | eqeq2d 2182 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧
ℎ ∈ Q))
→ (𝑥 = (𝑓𝐺𝑡) ↔ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
16 | 15 | expcom 115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → (𝑡
= (𝑔𝐺ℎ) → (𝑥 = (𝑓𝐺𝑡) ↔ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
17 | 16 | pm5.32d 447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑡
= (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
18 | 17 | 3expa 1198 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 ∈ Q ∧
𝑔 ∈ Q)
∧ ℎ ∈
Q) → ((𝑡
= (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
19 | 9, 18 | sylan2 284 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓 ∈ Q ∧
𝑔 ∈ Q)
∧ (𝐶 ∈
P ∧ ℎ
∈ (1st ‘𝐶))) → ((𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
20 | 19 | anassrs 398 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓 ∈ Q ∧
𝑔 ∈ Q)
∧ 𝐶 ∈
P) ∧ ℎ
∈ (1st ‘𝐶)) → ((𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
21 | 20 | rexbidva 2467 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ Q ∧
𝑔 ∈ Q)
∧ 𝐶 ∈
P) → (∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ ∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
22 | | r19.41v 2626 |
. . . . . . . . . . . . . . . . 17
⊢
(∃ℎ ∈
(1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))) |
23 | 21, 22 | bitr3di 194 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ Q ∧
𝑔 ∈ Q)
∧ 𝐶 ∈
P) → (∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
24 | 23 | an32s 563 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ Q ∧
𝐶 ∈ P)
∧ 𝑔 ∈
Q) → (∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
25 | 6, 24 | sylan2 284 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ Q ∧
𝐶 ∈ P)
∧ (𝐵 ∈
P ∧ 𝑔
∈ (1st ‘𝐵))) → (∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
26 | 25 | anassrs 398 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ Q ∧
𝐶 ∈ P)
∧ 𝐵 ∈
P) ∧ 𝑔
∈ (1st ‘𝐵)) → (∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
27 | 26 | rexbidva 2467 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ Q ∧
𝐶 ∈ P)
∧ 𝐵 ∈
P) → (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑔 ∈ (1st ‘𝐵)(∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
28 | | r19.41v 2626 |
. . . . . . . . . . . 12
⊢
(∃𝑔 ∈
(1st ‘𝐵)(∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))) |
29 | 27, 28 | bitrdi 195 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ Q ∧
𝐶 ∈ P)
∧ 𝐵 ∈
P) → (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
30 | 29 | an31s 565 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ 𝑓 ∈
Q) → (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
31 | 30 | exbidv 1818 |
. . . . . . . . 9
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ 𝑓 ∈
Q) → (∃𝑡∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑡(∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
32 | | genpelvl.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) |
33 | 32 | caovcl 6004 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔𝐺ℎ) ∈ Q) |
34 | | elisset 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔𝐺ℎ) ∈ Q → ∃𝑡 𝑡 = (𝑔𝐺ℎ)) |
35 | 33, 34 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ ∃𝑡 𝑡 = (𝑔𝐺ℎ)) |
36 | 35 | biantrurd 303 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ (∃𝑡 𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
37 | | 19.41v 1895 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
38 | 36, 37 | bitr4di 197 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
39 | 9, 38 | sylan2 284 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ Q ∧
(𝐶 ∈ P
∧ ℎ ∈
(1st ‘𝐶)))
→ (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
40 | 39 | anassrs 398 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔 ∈ Q ∧
𝐶 ∈ P)
∧ ℎ ∈
(1st ‘𝐶))
→ (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
41 | 40 | rexbidva 2467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ Q ∧
𝐶 ∈ P)
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃ℎ ∈ (1st ‘𝐶)∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
42 | | rexcom4 2753 |
. . . . . . . . . . . . . . . . 17
⊢
(∃ℎ ∈
(1st ‘𝐶)∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
43 | 41, 42 | bitrdi 195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ Q ∧
𝐶 ∈ P)
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
44 | 43 | ancoms 266 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ P ∧
𝑔 ∈ Q)
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
45 | 6, 44 | sylan2 284 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ P ∧
(𝐵 ∈ P
∧ 𝑔 ∈
(1st ‘𝐵)))
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
46 | 45 | anassrs 398 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ P ∧
𝐵 ∈ P)
∧ 𝑔 ∈
(1st ‘𝐵))
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
47 | 46 | rexbidva 2467 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑔 ∈ (1st ‘𝐵)∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
48 | 47 | ancoms 266 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑔 ∈ (1st ‘𝐵)∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
49 | | rexcom4 2753 |
. . . . . . . . . . 11
⊢
(∃𝑔 ∈
(1st ‘𝐵)∃𝑡∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
50 | 48, 49 | bitrdi 195 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
51 | 50 | adantr 274 |
. . . . . . . . 9
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ 𝑓 ∈
Q) → (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
52 | | df-rex 2454 |
. . . . . . . . . . 11
⊢
(∃𝑡 ∈
(1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑡(𝑡 ∈ (1st ‘(𝐵𝐹𝐶)) ∧ 𝑥 = (𝑓𝐺𝑡))) |
53 | | genpelvl.1 |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦𝐺𝑧))}〉) |
54 | 53, 32 | genpelvl 7461 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑡 ∈
(1st ‘(𝐵𝐹𝐶)) ↔ ∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ))) |
55 | 54 | anbi1d 462 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝑡 ∈
(1st ‘(𝐵𝐹𝐶)) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
56 | 55 | exbidv 1818 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (∃𝑡(𝑡 ∈ (1st
‘(𝐵𝐹𝐶)) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ ∃𝑡(∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
57 | 52, 56 | syl5bb 191 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (∃𝑡 ∈
(1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑡(∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
58 | 57 | adantr 274 |
. . . . . . . . 9
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ 𝑓 ∈
Q) → (∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑡(∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))) |
59 | 31, 51, 58 | 3bitr4rd 220 |
. . . . . . . 8
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ 𝑓 ∈
Q) → (∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
60 | 3, 59 | sylan2 284 |
. . . . . . 7
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ (𝐴 ∈
P ∧ 𝑓
∈ (1st ‘𝐴))) → (∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
61 | 60 | anassrs 398 |
. . . . . 6
⊢ ((((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ 𝐴 ∈
P) ∧ 𝑓
∈ (1st ‘𝐴)) → (∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
62 | 61 | rexbidva 2467 |
. . . . 5
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ 𝐴 ∈
P) → (∃𝑓 ∈ (1st ‘𝐴)∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
63 | 62 | ancoms 266 |
. . . 4
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐶 ∈
P)) → (∃𝑓 ∈ (1st ‘𝐴)∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
64 | 63 | 3impb 1194 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑓 ∈ (1st ‘𝐴)∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
65 | | genpassg.5 |
. . . . . 6
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓𝐹𝑔) ∈ P) |
66 | 65 | caovcl 6004 |
. . . . 5
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐵𝐹𝐶) ∈ P) |
67 | 53, 32 | genpelvl 7461 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
(𝐵𝐹𝐶) ∈ P) → (𝑥 ∈ (1st
‘(𝐴𝐹(𝐵𝐹𝐶))) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡))) |
68 | 66, 67 | sylan2 284 |
. . . 4
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐶 ∈
P)) → (𝑥
∈ (1st ‘(𝐴𝐹(𝐵𝐹𝐶))) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡))) |
69 | 68 | 3impb 1194 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑥
∈ (1st ‘(𝐴𝐹(𝐵𝐹𝐶))) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑡 ∈ (1st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡))) |
70 | | df-rex 2454 |
. . . . 5
⊢
(∃𝑡 ∈
(1st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ) ↔ ∃𝑡(𝑡 ∈ (1st ‘(𝐴𝐹𝐵)) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
71 | 53, 32 | genpelvl 7461 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑡 ∈
(1st ‘(𝐴𝐹𝐵)) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔))) |
72 | 71 | 3adant3 1012 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑡
∈ (1st ‘(𝐴𝐹𝐵)) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔))) |
73 | 72 | anbi1d 462 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑡
∈ (1st ‘(𝐴𝐹𝐵)) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
74 | 73 | exbidv 1818 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑡(𝑡 ∈ (1st ‘(𝐴𝐹𝐵)) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡(∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
75 | 70, 74 | syl5bb 191 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑡 ∈ (1st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
76 | 65 | caovcl 6004 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴𝐹𝐵) ∈ P) |
77 | 53, 32 | genpelvl 7461 |
. . . . . 6
⊢ (((𝐴𝐹𝐵) ∈ P ∧ 𝐶 ∈ P) →
(𝑥 ∈ (1st
‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑡 ∈ (1st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
78 | 76, 77 | sylan 281 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ 𝐶 ∈
P) → (𝑥
∈ (1st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑡 ∈ (1st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
79 | 78 | 3impa 1189 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑥
∈ (1st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑡 ∈ (1st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
80 | 32 | caovcl 6004 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓𝐺𝑔) ∈ Q) |
81 | | elisset 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓𝐺𝑔) ∈ Q → ∃𝑡 𝑡 = (𝑓𝐺𝑔)) |
82 | 80, 81 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ ∃𝑡 𝑡 = (𝑓𝐺𝑔)) |
83 | 82 | biantrurd 303 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ (∃𝑡 𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))) |
84 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = (𝑓𝐺𝑔) → (𝑡𝐺ℎ) = ((𝑓𝐺𝑔)𝐺ℎ)) |
85 | 84 | eqeq2d 2182 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝑓𝐺𝑔) → (𝑥 = (𝑡𝐺ℎ) ↔ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
86 | 85 | rexbidv 2471 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝑓𝐺𝑔) → (∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ) ↔ ∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
87 | 86 | pm5.32i 451 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
88 | 87 | exbii 1598 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
89 | | 19.41v 1895 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
90 | 88, 89 | bitri 183 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑡 𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
91 | 83, 90 | bitr4di 197 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
92 | 6, 91 | sylan2 284 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ Q ∧
(𝐵 ∈ P
∧ 𝑔 ∈
(1st ‘𝐵)))
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
93 | 92 | anassrs 398 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ Q ∧
𝐵 ∈ P)
∧ 𝑔 ∈
(1st ‘𝐵))
→ (∃ℎ ∈
(1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
94 | 93 | rexbidva 2467 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ Q ∧
𝐵 ∈ P)
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑔 ∈ (1st ‘𝐵)∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
95 | | rexcom4 2753 |
. . . . . . . . . . . . 13
⊢
(∃𝑔 ∈
(1st ‘𝐵)∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
96 | 94, 95 | bitrdi 195 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ Q ∧
𝐵 ∈ P)
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
97 | 96 | ancoms 266 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ P ∧
𝑓 ∈ Q)
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
98 | 3, 97 | sylan2 284 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ P ∧
(𝐴 ∈ P
∧ 𝑓 ∈
(1st ‘𝐴)))
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
99 | 98 | anassrs 398 |
. . . . . . . . 9
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ P)
∧ 𝑓 ∈
(1st ‘𝐴))
→ (∃𝑔 ∈
(1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
100 | 99 | rexbidva 2467 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ P)
→ (∃𝑓 ∈
(1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑡∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
101 | | rexcom4 2753 |
. . . . . . . 8
⊢
(∃𝑓 ∈
(1st ‘𝐴)∃𝑡∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
102 | 100, 101 | bitrdi 195 |
. . . . . . 7
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ P)
→ (∃𝑓 ∈
(1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
103 | | r19.41v 2626 |
. . . . . . . . . 10
⊢
(∃𝑔 ∈
(1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
104 | 103 | rexbii 2477 |
. . . . . . . . 9
⊢
(∃𝑓 ∈
(1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑓 ∈ (1st ‘𝐴)(∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
105 | | r19.41v 2626 |
. . . . . . . . 9
⊢
(∃𝑓 ∈
(1st ‘𝐴)(∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
106 | 104, 105 | bitri 183 |
. . . . . . . 8
⊢
(∃𝑓 ∈
(1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
107 | 106 | exbii 1598 |
. . . . . . 7
⊢
(∃𝑡∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡(∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ))) |
108 | 102, 107 | bitrdi 195 |
. . . . . 6
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ P)
→ (∃𝑓 ∈
(1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
109 | 108 | ancoms 266 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑓 ∈
(1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
110 | 109 | 3adant3 1012 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))) |
111 | 75, 79, 110 | 3bitr4d 219 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑥
∈ (1st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑓 ∈ (1st ‘𝐴)∃𝑔 ∈ (1st ‘𝐵)∃ℎ ∈ (1st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))) |
112 | 64, 69, 111 | 3bitr4rd 220 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑥
∈ (1st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ 𝑥 ∈ (1st ‘(𝐴𝐹(𝐵𝐹𝐶))))) |
113 | 112 | eqrdv 2168 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (1st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1st ‘(𝐴𝐹(𝐵𝐹𝐶)))) |