Proof of Theorem bnj1417
Step | Hyp | Ref
| Expression |
1 | | bnj1417.1 |
. . . 4
⊢ (𝜑 ↔ 𝑅 FrSe 𝐴) |
2 | 1 | biimpi 205 |
. . 3
⊢ (𝜑 → 𝑅 FrSe 𝐴) |
3 | | bnj1417.4 |
. . . . . 6
⊢ (𝜃 ↔ (𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒)) |
4 | | bnj1418 30362 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑥𝑅𝑥) |
5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜃 ∧ 𝑥 ∈ pred(𝑥, 𝐴, 𝑅)) → 𝑥𝑅𝑥) |
6 | 3, 2 | bnj835 30083 |
. . . . . . . . . . . 12
⊢ (𝜃 → 𝑅 FrSe 𝐴) |
7 | | df-bnj15 30012 |
. . . . . . . . . . . . 13
⊢ (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴)) |
8 | 7 | simplbi 475 |
. . . . . . . . . . . 12
⊢ (𝑅 FrSe 𝐴 → 𝑅 Fr 𝐴) |
9 | 6, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜃 → 𝑅 Fr 𝐴) |
10 | | bnj213 30206 |
. . . . . . . . . . . 12
⊢
pred(𝑥, 𝐴, 𝑅) ⊆ 𝐴 |
11 | 10 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑥 ∈ 𝐴) |
12 | | frirr 5015 |
. . . . . . . . . . 11
⊢ ((𝑅 Fr 𝐴 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) |
13 | 9, 11, 12 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜃 ∧ 𝑥 ∈ pred(𝑥, 𝐴, 𝑅)) → ¬ 𝑥𝑅𝑥) |
14 | 5, 13 | pm2.65da 598 |
. . . . . . . . 9
⊢ (𝜃 → ¬ 𝑥 ∈ pred(𝑥, 𝐴, 𝑅)) |
15 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦𝜑 |
16 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 |
17 | | bnj1417.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓)) |
18 | 17 | bnj1095 30106 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → ∀𝑦𝜒) |
19 | 18 | nf5i 2011 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦𝜒 |
20 | 15, 16, 19 | nf3an 1819 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒) |
21 | 3, 20 | nfxfr 1771 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝜃 |
22 | 6 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴) |
23 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) |
24 | 10, 23 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴) |
25 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) |
26 | | bnj1125 30314 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑥, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅)) |
27 | 22, 24, 25, 26 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑥, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅)) |
28 | | bnj1147 30316 |
. . . . . . . . . . . . . . . . . 18
⊢
trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
29 | 28, 25 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑥 ∈ 𝐴) |
30 | | bnj906 30254 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ⊆ trCl(𝑥, 𝐴, 𝑅)) |
31 | 22, 29, 30 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑥, 𝐴, 𝑅) ⊆ trCl(𝑥, 𝐴, 𝑅)) |
32 | 31, 23 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ trCl(𝑥, 𝐴, 𝑅)) |
33 | 27, 32 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ trCl(𝑦, 𝐴, 𝑅)) |
34 | 17 | biimpi 205 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓)) |
35 | 3, 34 | bnj837 30085 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓)) |
36 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓)) |
37 | | bnj1418 30362 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑦𝑅𝑥) |
38 | 37 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦𝑅𝑥) |
39 | | rsp 2913 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓) → (𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓))) |
40 | 36, 24, 38, 39 | syl3c 64 |
. . . . . . . . . . . . . . 15
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → [𝑦 / 𝑥]𝜓) |
41 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
42 | | bnj1417.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜓 ↔ ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅)) |
43 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝑥 ∈ trCl(𝑥, 𝐴, 𝑅) ↔ 𝑦 ∈ trCl(𝑥, 𝐴, 𝑅))) |
44 | | bnj1318 30347 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → trCl(𝑥, 𝐴, 𝑅) = trCl(𝑦, 𝐴, 𝑅)) |
45 | 44 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝑦 ∈ trCl(𝑥, 𝐴, 𝑅) ↔ 𝑦 ∈ trCl(𝑦, 𝐴, 𝑅))) |
46 | 43, 45 | bitrd 267 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ∈ trCl(𝑥, 𝐴, 𝑅) ↔ 𝑦 ∈ trCl(𝑦, 𝐴, 𝑅))) |
47 | 46 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅) ↔ ¬ 𝑦 ∈ trCl(𝑦, 𝐴, 𝑅))) |
48 | 42, 47 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝜓 ↔ ¬ 𝑦 ∈ trCl(𝑦, 𝐴, 𝑅))) |
49 | 41, 48 | sbcie 3437 |
. . . . . . . . . . . . . . 15
⊢
([𝑦 / 𝑥]𝜓 ↔ ¬ 𝑦 ∈ trCl(𝑦, 𝐴, 𝑅)) |
50 | 40, 49 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) ∧ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) → ¬ 𝑦 ∈ trCl(𝑦, 𝐴, 𝑅)) |
51 | 33, 50 | pm2.65da 598 |
. . . . . . . . . . . . 13
⊢ ((𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → ¬ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) |
52 | 51 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜃 → (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ¬ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅))) |
53 | 21, 52 | ralrimi 2940 |
. . . . . . . . . . 11
⊢ (𝜃 → ∀𝑦 ∈ pred (𝑥, 𝐴, 𝑅) ¬ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) |
54 | | ralnex 2975 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
pred (𝑥, 𝐴, 𝑅) ¬ 𝑥 ∈ trCl(𝑦, 𝐴, 𝑅) ↔ ¬ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) |
55 | 53, 54 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜃 → ¬ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) |
56 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ↔ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝑥 ∈ trCl(𝑦, 𝐴, 𝑅)) |
57 | 55, 56 | sylnibr 318 |
. . . . . . . . 9
⊢ (𝜃 → ¬ 𝑥 ∈ ∪
𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) |
58 | | ioran 510 |
. . . . . . . . 9
⊢ (¬
(𝑥 ∈ pred(𝑥, 𝐴, 𝑅) ∨ 𝑥 ∈ ∪
𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ↔ (¬ 𝑥 ∈ pred(𝑥, 𝐴, 𝑅) ∧ ¬ 𝑥 ∈ ∪
𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))) |
59 | 14, 57, 58 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝜃 → ¬ (𝑥 ∈ pred(𝑥, 𝐴, 𝑅) ∨ 𝑥 ∈ ∪
𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))) |
60 | 3 | simp2bi 1070 |
. . . . . . . . . . 11
⊢ (𝜃 → 𝑥 ∈ 𝐴) |
61 | | bnj1417.5 |
. . . . . . . . . . . 12
⊢ 𝐵 = ( pred(𝑥, 𝐴, 𝑅) ∪ ∪
𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) |
62 | 61 | bnj1414 30359 |
. . . . . . . . . . 11
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → trCl(𝑥, 𝐴, 𝑅) = 𝐵) |
63 | 6, 60, 62 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜃 → trCl(𝑥, 𝐴, 𝑅) = 𝐵) |
64 | 63 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝜃 → (𝑥 ∈ trCl(𝑥, 𝐴, 𝑅) ↔ 𝑥 ∈ 𝐵)) |
65 | 61 | bnj1138 30113 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ pred(𝑥, 𝐴, 𝑅) ∨ 𝑥 ∈ ∪
𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))) |
66 | 64, 65 | syl6bb 275 |
. . . . . . . 8
⊢ (𝜃 → (𝑥 ∈ trCl(𝑥, 𝐴, 𝑅) ↔ (𝑥 ∈ pred(𝑥, 𝐴, 𝑅) ∨ 𝑥 ∈ ∪
𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))) |
67 | 59, 66 | mtbird 314 |
. . . . . . 7
⊢ (𝜃 → ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅)) |
68 | 67, 42 | sylibr 223 |
. . . . . 6
⊢ (𝜃 → 𝜓) |
69 | 3, 68 | sylbir 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒) → 𝜓) |
70 | 69 | 3exp 1256 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜒 → 𝜓))) |
71 | 70 | ralrimiv 2948 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜒 → 𝜓)) |
72 | 17 | bnj1204 30334 |
. . 3
⊢ ((𝑅 FrSe 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜒 → 𝜓)) → ∀𝑥 ∈ 𝐴 𝜓) |
73 | 2, 71, 72 | syl2anc 691 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
74 | 42 | ralbii 2963 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅)) |
75 | 73, 74 | sylib 207 |
1
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅)) |