Step | Hyp | Ref
| Expression |
1 | | bnj1312.5 |
. . 3
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} |
2 | | bnj1312.6 |
. . . 4
⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) |
3 | 2 | simplbi 501 |
. . . . . . 7
⊢ (𝜓 → 𝑅 FrSe 𝐴) |
4 | 1 | ssrab3 3971 |
. . . . . . . 8
⊢ 𝐷 ⊆ 𝐴 |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ (𝜓 → 𝐷 ⊆ 𝐴) |
6 | 2 | simprbi 500 |
. . . . . . 7
⊢ (𝜓 → 𝐷 ≠ ∅) |
7 | 1 | bnj1230 32353 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐷 → ∀𝑥 𝑤 ∈ 𝐷) |
8 | 7 | bnj1228 32562 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝐷 ≠ ∅) → ∃𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥) |
9 | 3, 5, 6, 8 | syl3anc 1372 |
. . . . . 6
⊢ (𝜓 → ∃𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥) |
10 | | bnj1312.7 |
. . . . . 6
⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) |
11 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑅 FrSe 𝐴 |
12 | 7 | nfcii 2883 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐷 |
13 | | nfcv 2899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∅ |
14 | 12, 13 | nfne 3034 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐷 ≠ ∅ |
15 | 11, 14 | nfan 1906 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅) |
16 | 2, 15 | nfxfr 1859 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
17 | 16 | nf5ri 2197 |
. . . . . 6
⊢ (𝜓 → ∀𝑥𝜓) |
18 | 9, 10, 17 | bnj1521 32402 |
. . . . 5
⊢ (𝜓 → ∃𝑥𝜒) |
19 | 10 | simp2bi 1147 |
. . . . 5
⊢ (𝜒 → 𝑥 ∈ 𝐷) |
20 | 1 | bnj1538 32406 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ¬ ∃𝑓𝜏) |
21 | | bnj1312.1 |
. . . . . . . . 9
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
22 | | bnj1312.2 |
. . . . . . . . 9
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
23 | | bnj1312.3 |
. . . . . . . . 9
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
24 | | bnj1312.4 |
. . . . . . . . 9
⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
25 | | bnj1312.8 |
. . . . . . . . 9
⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) |
26 | | bnj1312.9 |
. . . . . . . . 9
⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
27 | | bnj1312.10 |
. . . . . . . . 9
⊢ 𝑃 = ∪
𝐻 |
28 | | bnj1312.11 |
. . . . . . . . 9
⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
29 | | bnj1312.12 |
. . . . . . . . 9
⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) |
30 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29 | bnj1489 32607 |
. . . . . . . 8
⊢ (𝜒 → 𝑄 ∈ V) |
31 | | bnj1312.13 |
. . . . . . . . . . 11
⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 |
32 | | bnj1312.14 |
. . . . . . . . . . 11
⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) |
33 | 10, 3 | bnj835 32309 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → 𝑅 FrSe 𝐴) |
34 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27 | bnj1384 32583 |
. . . . . . . . . . . . . 14
⊢ (𝑅 FrSe 𝐴 → Fun 𝑃) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜒 → Fun 𝑃) |
36 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27 | bnj1415 32589 |
. . . . . . . . . . . . 13
⊢ (𝜒 → dom 𝑃 = trCl(𝑥, 𝐴, 𝑅)) |
37 | 35, 36 | bnj1422 32388 |
. . . . . . . . . . . 12
⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅)) |
38 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 36 | bnj1416 32590 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
39 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 35, 38, 36 | bnj1421 32593 |
. . . . . . . . . . . . 13
⊢ (𝜒 → Fun 𝑄) |
40 | 39, 38 | bnj1422 32388 |
. . . . . . . . . . . 12
⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
41 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 31, 32, 37, 40 | bnj1423 32602 |
. . . . . . . . . . 11
⊢ (𝜒 → ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)) |
42 | 32 | fneq2i 6436 |
. . . . . . . . . . . 12
⊢ (𝑄 Fn 𝐸 ↔ 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
43 | 40, 42 | sylibr 237 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑄 Fn 𝐸) |
44 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 31, 32 | bnj1452 32603 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝐸 ∈ 𝐵) |
45 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 31, 32, 30, 41, 43, 44 | bnj1463 32606 |
. . . . . . . . . 10
⊢ (𝜒 → 𝑄 ∈ 𝐶) |
46 | 45, 38 | jca 515 |
. . . . . . . . 9
⊢ (𝜒 → (𝑄 ∈ 𝐶 ∧ dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
47 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 46 | bnj1491 32608 |
. . . . . . . 8
⊢ ((𝜒 ∧ 𝑄 ∈ V) → ∃𝑓(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
48 | 30, 47 | mpdan 687 |
. . . . . . 7
⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
49 | 48, 24 | bnj1198 32346 |
. . . . . 6
⊢ (𝜒 → ∃𝑓𝜏) |
50 | 20, 49 | nsyl3 140 |
. . . . 5
⊢ (𝜒 → ¬ 𝑥 ∈ 𝐷) |
51 | 18, 19, 50 | bnj1304 32370 |
. . . 4
⊢ ¬
𝜓 |
52 | 2, 51 | bnj1541 32407 |
. . 3
⊢ (𝑅 FrSe 𝐴 → 𝐷 = ∅) |
53 | 1, 52 | bnj1476 32398 |
. 2
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓𝜏) |
54 | 24 | exbii 1854 |
. . . 4
⊢
(∃𝑓𝜏 ↔ ∃𝑓(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
55 | | df-rex 3059 |
. . . 4
⊢
(∃𝑓 ∈
𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) ↔ ∃𝑓(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
56 | 54, 55 | bitr4i 281 |
. . 3
⊢
(∃𝑓𝜏 ↔ ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
57 | 56 | ralbii 3080 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃𝑓𝜏 ↔ ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
58 | 53, 57 | sylib 221 |
1
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |