Proof of Theorem frrlem14
Step | Hyp | Ref
| Expression |
1 | | frrlem11.1 |
. . . 4
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
2 | | frrlem11.2 |
. . . 4
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) |
3 | 1, 2 | frrlem7 8108 |
. . 3
⊢ dom 𝐹 ⊆ 𝐴 |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → dom 𝐹 ⊆ 𝐴) |
5 | | eldifn 4062 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹) |
6 | 5 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ dom 𝐹) |
7 | | frrlem11.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) |
8 | | frrlem11.4 |
. . . . . . . . . . . 12
⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) |
9 | | frrlem12.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 Fr 𝐴) |
10 | | frrlem12.6 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) |
11 | | frrlem12.7 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) |
12 | | frrlem13.8 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V) |
13 | | frrlem13.9 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴) |
14 | 1, 2, 7, 8, 9, 10,
11, 12, 13 | frrlem13 8114 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵) |
15 | | elssuni 4871 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝐵 → 𝐶 ⊆ ∪ 𝐵) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ⊆ ∪ 𝐵) |
17 | 1, 2 | frrlem5 8106 |
. . . . . . . . . 10
⊢ 𝐹 = ∪
𝐵 |
18 | 16, 17 | sseqtrrdi 3972 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ⊆ 𝐹) |
19 | | dmss 5811 |
. . . . . . . . 9
⊢ (𝐶 ⊆ 𝐹 → dom 𝐶 ⊆ dom 𝐹) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → dom 𝐶 ⊆ dom 𝐹) |
21 | | ssun2 4107 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) |
22 | | vsnid 4598 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ {𝑧} |
23 | 21, 22 | sselii 3918 |
. . . . . . . . . 10
⊢ 𝑧 ∈ (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) |
24 | 8 | dmeqi 5813 |
. . . . . . . . . . 11
⊢ dom 𝐶 = dom ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) |
25 | | dmun 5819 |
. . . . . . . . . . 11
⊢ dom
((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) = (dom (𝐹 ↾ 𝑆) ∪ dom {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) |
26 | | ovex 7308 |
. . . . . . . . . . . . 13
⊢ (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V |
27 | 26 | dmsnop 6119 |
. . . . . . . . . . . 12
⊢ dom
{〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} = {𝑧} |
28 | 27 | uneq2i 4094 |
. . . . . . . . . . 11
⊢ (dom
(𝐹 ↾ 𝑆) ∪ dom {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) = (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) |
29 | 24, 25, 28 | 3eqtri 2770 |
. . . . . . . . . 10
⊢ dom 𝐶 = (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) |
30 | 23, 29 | eleqtrri 2838 |
. . . . . . . . 9
⊢ 𝑧 ∈ dom 𝐶 |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ dom 𝐶) |
32 | 20, 31 | sseldd 3922 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ dom 𝐹) |
33 | 32 | expr 457 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → 𝑧 ∈ dom 𝐹)) |
34 | 6, 33 | mtod 197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) |
35 | 34 | nrexdv 3198 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) |
36 | | df-ne 2944 |
. . . . . 6
⊢ ((𝐴 ∖ dom 𝐹) ≠ ∅ ↔ ¬ (𝐴 ∖ dom 𝐹) = ∅) |
37 | | frrlem14.10 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) |
38 | 36, 37 | sylan2br 595 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐴 ∖ dom 𝐹) = ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) |
39 | 38 | ex 413 |
. . . 4
⊢ (𝜑 → (¬ (𝐴 ∖ dom 𝐹) = ∅ → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) |
40 | 35, 39 | mt3d 148 |
. . 3
⊢ (𝜑 → (𝐴 ∖ dom 𝐹) = ∅) |
41 | | ssdif0 4297 |
. . 3
⊢ (𝐴 ⊆ dom 𝐹 ↔ (𝐴 ∖ dom 𝐹) = ∅) |
42 | 40, 41 | sylibr 233 |
. 2
⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) |
43 | 4, 42 | eqssd 3938 |
1
⊢ (𝜑 → dom 𝐹 = 𝐴) |