Step | Hyp | Ref
| Expression |
1 | | nfv 1538 |
. . 3
โข
โฒ๐ฆ(๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) |
2 | | nfre1 2530 |
. . 3
โข
โฒ๐ฆโ๐ฆ โ ฯ ((๐ด +Q0
([โจ๐ฆ,
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) |
3 | | prarloclemlo 7506 |
. . . . 5
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โ (((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
4 | | prarloclemup 7507 |
. . . . 5
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ((๐ฆ +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐ โ (((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
5 | | prarloclemlt 7505 |
. . . . . 6
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) <Q (๐ด +Q
([โจ((๐ฆ +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐))) |
6 | | prloc 7503 |
. . . . . . . . 9
โข
((โจ๐ฟ, ๐โฉ โ P
โง (๐ด
+Q ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐)) <Q (๐ด +Q
([โจ((๐ฆ +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐))) โ ((๐ด +Q ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โจ (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
7 | 6 | ex 115 |
. . . . . . . 8
โข
(โจ๐ฟ, ๐โฉ โ P
โ ((๐ด
+Q ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐)) <Q (๐ด +Q
([โจ((๐ฆ +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ((๐ด +Q ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โจ (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
8 | 7 | 3ad2ant1 1019 |
. . . . . . 7
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ด โ ๐ฟ โง ๐ โ Q) โ ((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) <Q (๐ด +Q
([โจ((๐ฆ +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ((๐ด +Q ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โจ (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
9 | 8 | ad2antlr 489 |
. . . . . 6
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) <Q (๐ด +Q
([โจ((๐ฆ +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ((๐ด +Q ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โจ (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
10 | 5, 9 | mpd 13 |
. . . . 5
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โจ (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
11 | 3, 4, 10 | mpjaod 719 |
. . . 4
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (((๐ด +Q0
([โจ๐ฆ,
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
12 | 11 | ex 115 |
. . 3
โข ((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โ (๐ฆ โ ฯ โ (((๐ด +Q0
([โจ๐ฆ,
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
13 | 1, 2, 12 | rexlimd 2601 |
. 2
โข ((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โ
(โ๐ฆ โ ฯ
((๐ด
+Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
14 | 13 | imp 124 |
1
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง โ๐ฆ โ ฯ ((๐ด +Q0
([โจ๐ฆ,
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |