Step | Hyp | Ref
| Expression |
1 | | istrkg.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | istrkg.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
3 | | simpl 486 |
. . . . 5
⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃) |
4 | 3 | eqcomd 2745 |
. . . 4
⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑃 = 𝑝) |
5 | 4 | adantr 484 |
. . . . 5
⊢ (((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) → 𝑃 = 𝑝) |
6 | 5 | adantr 484 |
. . . . . 6
⊢ ((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → 𝑃 = 𝑝) |
7 | 6 | adantr 484 |
. . . . . . 7
⊢
(((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → 𝑃 = 𝑝) |
8 | 7 | adantr 484 |
. . . . . . . 8
⊢
((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) → 𝑃 = 𝑝) |
9 | | simp-6r 788 |
. . . . . . . . . . . . 13
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → 𝑖 = 𝐼) |
10 | 9 | eqcomd 2745 |
. . . . . . . . . . . 12
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → 𝐼 = 𝑖) |
11 | 10 | oveqd 7200 |
. . . . . . . . . . 11
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → (𝑥𝐼𝑣) = (𝑥𝑖𝑣)) |
12 | 11 | eleq2d 2819 |
. . . . . . . . . 10
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → (𝑢 ∈ (𝑥𝐼𝑣) ↔ 𝑢 ∈ (𝑥𝑖𝑣))) |
13 | 10 | oveqd 7200 |
. . . . . . . . . . 11
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → (𝑦𝐼𝑧) = (𝑦𝑖𝑧)) |
14 | 13 | eleq2d 2819 |
. . . . . . . . . 10
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → (𝑢 ∈ (𝑦𝐼𝑧) ↔ 𝑢 ∈ (𝑦𝑖𝑧))) |
15 | 12, 14 | 3anbi12d 1438 |
. . . . . . . . 9
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) ↔ (𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢))) |
16 | 8 | adantr 484 |
. . . . . . . . . 10
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → 𝑃 = 𝑝) |
17 | 16 | adantr 484 |
. . . . . . . . . . 11
⊢
((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) → 𝑃 = 𝑝) |
18 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → 𝑖 = 𝐼) |
19 | 18 | eqcomd 2745 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → 𝐼 = 𝑖) |
20 | 19 | oveqd 7200 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (𝑥𝐼𝑎) = (𝑥𝑖𝑎)) |
21 | 20 | eleq2d 2819 |
. . . . . . . . . . . 12
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (𝑦 ∈ (𝑥𝐼𝑎) ↔ 𝑦 ∈ (𝑥𝑖𝑎))) |
22 | 19 | oveqd 7200 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (𝑥𝐼𝑏) = (𝑥𝑖𝑏)) |
23 | 22 | eleq2d 2819 |
. . . . . . . . . . . 12
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (𝑧 ∈ (𝑥𝐼𝑏) ↔ 𝑧 ∈ (𝑥𝑖𝑏))) |
24 | 19 | oveqd 7200 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (𝑎𝐼𝑏) = (𝑎𝑖𝑏)) |
25 | 24 | eleq2d 2819 |
. . . . . . . . . . . 12
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → (𝑣 ∈ (𝑎𝐼𝑏) ↔ 𝑣 ∈ (𝑎𝑖𝑏))) |
26 | 21, 23, 25 | 3anbi123d 1437 |
. . . . . . . . . . 11
⊢
(((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) → ((𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))) |
27 | 17, 26 | rexeqbidva 3324 |
. . . . . . . . . 10
⊢
((((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑎 ∈ 𝑃) → (∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))) |
28 | 16, 27 | rexeqbidva 3324 |
. . . . . . . . 9
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))) |
29 | 15, 28 | imbi12d 348 |
. . . . . . . 8
⊢
(((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) → (((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))))) |
30 | 8, 29 | raleqbidva 3323 |
. . . . . . 7
⊢
((((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑢 ∈ 𝑃) → (∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))))) |
31 | 7, 30 | raleqbidva 3323 |
. . . . . 6
⊢
(((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))))) |
32 | 6, 31 | raleqbidva 3323 |
. . . . 5
⊢ ((((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → (∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))))) |
33 | 5, 32 | raleqbidva 3323 |
. . . 4
⊢ (((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) ∧ 𝑥 ∈ 𝑃) → (∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))))) |
34 | 4, 33 | raleqbidva 3323 |
. . 3
⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))))) |
35 | 1, 2, 34 | sbcie2s 16656 |
. 2
⊢ (𝑓 = 𝐺 → ([(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) ↔ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
36 | | df-trkge 26410 |
. 2
⊢
TarskiGE = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))} |
37 | 35, 36 | elab4g 3583 |
1
⊢ (𝐺 ∈ TarskiGE
↔ (𝐺 ∈ V ∧
∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |