Proof of Theorem frrlem14
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frrlem11.1 | . . . 4
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | 
| 2 |  | frrlem11.2 | . . . 4
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) | 
| 3 | 1, 2 | frrlem7 8317 | . . 3
⊢ dom 𝐹 ⊆ 𝐴 | 
| 4 | 3 | a1i 11 | . 2
⊢ (𝜑 → dom 𝐹 ⊆ 𝐴) | 
| 5 |  | eldifn 4132 | . . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹) | 
| 6 | 5 | adantl 481 | . . . . . 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 8323 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵) | 
| 15 |  | elssuni 4937 | . . . . . . . . . . 11
⊢ (𝐶 ∈ 𝐵 → 𝐶 ⊆ ∪ 𝐵) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ⊆ ∪ 𝐵) | 
| 17 | 1, 2 | frrlem5 8315 | . . . . . . . . . 10
⊢ 𝐹 = ∪
𝐵 | 
| 18 | 16, 17 | sseqtrrdi 4025 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ⊆ 𝐹) | 
| 19 |  | dmss 5913 | . . . . . . . . 9
⊢ (𝐶 ⊆ 𝐹 → dom 𝐶 ⊆ dom 𝐹) | 
| 20 | 18, 19 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → dom 𝐶 ⊆ dom 𝐹) | 
| 21 |  | ssun2 4179 | . . . . . . . . . . 11
⊢ {𝑧} ⊆ (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) | 
| 22 |  | vsnid 4663 | . . . . . . . . . . 11
⊢ 𝑧 ∈ {𝑧} | 
| 23 | 21, 22 | sselii 3980 | . . . . . . . . . 10
⊢ 𝑧 ∈ (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) | 
| 24 | 8 | dmeqi 5915 | . . . . . . . . . . 11
⊢ dom 𝐶 = dom ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) | 
| 25 |  | dmun 5921 | . . . . . . . . . . 11
⊢ dom
((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) = (dom (𝐹 ↾ 𝑆) ∪ dom {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) | 
| 26 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢ (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V | 
| 27 | 26 | dmsnop 6236 | . . . . . . . . . . . 12
⊢ dom
{〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} = {𝑧} | 
| 28 | 27 | uneq2i 4165 | . . . . . . . . . . 11
⊢ (dom
(𝐹 ↾ 𝑆) ∪ dom {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) = (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) | 
| 29 | 24, 25, 28 | 3eqtri 2769 | . . . . . . . . . 10
⊢ dom 𝐶 = (dom (𝐹 ↾ 𝑆) ∪ {𝑧}) | 
| 30 | 23, 29 | eleqtrri 2840 | . . . . . . . . 9
⊢ 𝑧 ∈ dom 𝐶 | 
| 31 | 30 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ dom 𝐶) | 
| 32 | 20, 31 | sseldd 3984 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ dom 𝐹) | 
| 33 | 32 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → 𝑧 ∈ dom 𝐹)) | 
| 34 | 6, 33 | mtod 198 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 35 | 34 | nrexdv 3149 | . . . 4
⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 36 |  | df-ne 2941 | . . . . . 6
⊢ ((𝐴 ∖ dom 𝐹) ≠ ∅ ↔ ¬ (𝐴 ∖ dom 𝐹) = ∅) | 
| 37 |  | frrlem14.10 | . . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 38 | 36, 37 | sylan2br 595 | . . . . 5
⊢ ((𝜑 ∧ ¬ (𝐴 ∖ dom 𝐹) = ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 39 | 38 | ex 412 | . . . 4
⊢ (𝜑 → (¬ (𝐴 ∖ dom 𝐹) = ∅ → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) | 
| 40 | 35, 39 | mt3d 148 | . . 3
⊢ (𝜑 → (𝐴 ∖ dom 𝐹) = ∅) | 
| 41 |  | ssdif0 4366 | . . 3
⊢ (𝐴 ⊆ dom 𝐹 ↔ (𝐴 ∖ dom 𝐹) = ∅) | 
| 42 | 40, 41 | sylibr 234 | . 2
⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) | 
| 43 | 4, 42 | eqssd 4001 | 1
⊢ (𝜑 → dom 𝐹 = 𝐴) |