Detailed syntax breakdown of Definition df-inag
Step | Hyp | Ref
| Expression |
1 | | cinag 27207 |
. 2
class
inA |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vp |
. . . . . . . 8
setvar 𝑝 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑝 |
6 | 2 | cv 1541 |
. . . . . . . 8
class 𝑔 |
7 | | cbs 16923 |
. . . . . . . 8
class
Base |
8 | 6, 7 | cfv 6432 |
. . . . . . 7
class
(Base‘𝑔) |
9 | 5, 8 | wcel 2110 |
. . . . . 6
wff 𝑝 ∈ (Base‘𝑔) |
10 | | vt |
. . . . . . . 8
setvar 𝑡 |
11 | 10 | cv 1541 |
. . . . . . 7
class 𝑡 |
12 | | cc0 10882 |
. . . . . . . . 9
class
0 |
13 | | c3 12040 |
. . . . . . . . 9
class
3 |
14 | | cfzo 13393 |
. . . . . . . . 9
class
..^ |
15 | 12, 13, 14 | co 7272 |
. . . . . . . 8
class
(0..^3) |
16 | | cmap 8607 |
. . . . . . . 8
class
↑m |
17 | 8, 15, 16 | co 7272 |
. . . . . . 7
class
((Base‘𝑔)
↑m (0..^3)) |
18 | 11, 17 | wcel 2110 |
. . . . . 6
wff 𝑡 ∈ ((Base‘𝑔) ↑m
(0..^3)) |
19 | 9, 18 | wa 396 |
. . . . 5
wff (𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m
(0..^3))) |
20 | 12, 11 | cfv 6432 |
. . . . . . . 8
class (𝑡‘0) |
21 | | c1 10883 |
. . . . . . . . 9
class
1 |
22 | 21, 11 | cfv 6432 |
. . . . . . . 8
class (𝑡‘1) |
23 | 20, 22 | wne 2945 |
. . . . . . 7
wff (𝑡‘0) ≠ (𝑡‘1) |
24 | | c2 12039 |
. . . . . . . . 9
class
2 |
25 | 24, 11 | cfv 6432 |
. . . . . . . 8
class (𝑡‘2) |
26 | 25, 22 | wne 2945 |
. . . . . . 7
wff (𝑡‘2) ≠ (𝑡‘1) |
27 | 5, 22 | wne 2945 |
. . . . . . 7
wff 𝑝 ≠ (𝑡‘1) |
28 | 23, 26, 27 | w3a 1086 |
. . . . . 6
wff ((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) |
29 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
30 | 29 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
31 | | citv 26805 |
. . . . . . . . . . 11
class
Itv |
32 | 6, 31 | cfv 6432 |
. . . . . . . . . 10
class
(Itv‘𝑔) |
33 | 20, 25, 32 | co 7272 |
. . . . . . . . 9
class ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) |
34 | 30, 33 | wcel 2110 |
. . . . . . . 8
wff 𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) |
35 | 30, 22 | wceq 1542 |
. . . . . . . . 9
wff 𝑥 = (𝑡‘1) |
36 | | chlg 26972 |
. . . . . . . . . . . 12
class
hlG |
37 | 6, 36 | cfv 6432 |
. . . . . . . . . . 11
class
(hlG‘𝑔) |
38 | 22, 37 | cfv 6432 |
. . . . . . . . . 10
class
((hlG‘𝑔)‘(𝑡‘1)) |
39 | 30, 5, 38 | wbr 5079 |
. . . . . . . . 9
wff 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝 |
40 | 35, 39 | wo 844 |
. . . . . . . 8
wff (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝) |
41 | 34, 40 | wa 396 |
. . . . . . 7
wff (𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)) |
42 | 41, 29, 8 | wrex 3067 |
. . . . . 6
wff
∃𝑥 ∈
(Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)) |
43 | 28, 42 | wa 396 |
. . . . 5
wff (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))) |
44 | 19, 43 | wa 396 |
. . . 4
wff ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)))) |
45 | 44, 4, 10 | copab 5141 |
. . 3
class
{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))} |
46 | 2, 3, 45 | cmpt 5162 |
. 2
class (𝑔 ∈ V ↦ {〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))}) |
47 | 1, 46 | wceq 1542 |
1
wff inA =
(𝑔 ∈ V ↦
{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))}) |