Proof of Theorem tfrlemibxssdm
Step | Hyp | Ref
| Expression |
1 | | tfrlemi1.5 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) |
2 | | tfrlemi1.4 |
. . . 4
⊢ (𝜑 → 𝑥 ∈ On) |
3 | | tfrlemisucfn.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) |
4 | 3 | tfrlem3-2d 6291 |
. . . . . . . . . . 11
⊢ (𝜑 → (Fun 𝐹 ∧ (𝐹‘𝑔) ∈ V)) |
5 | 4 | simprd 113 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑔) ∈ V) |
6 | 5 | 3ad2ant1 1013 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → (𝐹‘𝑔) ∈ V) |
7 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
8 | | opexg 4213 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ V ∧ (𝐹‘𝑔) ∈ V) → 〈𝑧, (𝐹‘𝑔)〉 ∈ V) |
9 | 7, 5, 8 | sylancr 412 |
. . . . . . . . . . . 12
⊢ (𝜑 → 〈𝑧, (𝐹‘𝑔)〉 ∈ V) |
10 | | snidg 3612 |
. . . . . . . . . . . 12
⊢
(〈𝑧, (𝐹‘𝑔)〉 ∈ V → 〈𝑧, (𝐹‘𝑔)〉 ∈ {〈𝑧, (𝐹‘𝑔)〉}) |
11 | | elun2 3295 |
. . . . . . . . . . . 12
⊢
(〈𝑧, (𝐹‘𝑔)〉 ∈ {〈𝑧, (𝐹‘𝑔)〉} → 〈𝑧, (𝐹‘𝑔)〉 ∈ (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) |
12 | 9, 10, 11 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈𝑧, (𝐹‘𝑔)〉 ∈ (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) |
13 | 12 | 3ad2ant1 1013 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → 〈𝑧, (𝐹‘𝑔)〉 ∈ (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) |
14 | | simp2r 1019 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → 𝑧 ∈ 𝑥) |
15 | | simp3l 1020 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → 𝑔 Fn 𝑧) |
16 | | onelon 4369 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ On) |
17 | | rspe 2519 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ On ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) |
18 | 16, 17 | sylan 281 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) |
19 | | tfrlemisucfn.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
20 | | vex 2733 |
. . . . . . . . . . . . . . 15
⊢ 𝑔 ∈ V |
21 | 19, 20 | tfrlem3a 6289 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) |
22 | 18, 21 | sylibr 133 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → 𝑔 ∈ 𝐴) |
23 | 22 | 3adant1 1010 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → 𝑔 ∈ 𝐴) |
24 | 14, 15, 23 | 3jca 1172 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → (𝑧 ∈ 𝑥 ∧ 𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴)) |
25 | | snexg 4170 |
. . . . . . . . . . . . . 14
⊢
(〈𝑧, (𝐹‘𝑔)〉 ∈ V → {〈𝑧, (𝐹‘𝑔)〉} ∈ V) |
26 | | unexg 4428 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ V ∧ {〈𝑧, (𝐹‘𝑔)〉} ∈ V) → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ V) |
27 | 20, 26 | mpan 422 |
. . . . . . . . . . . . . 14
⊢
({〈𝑧, (𝐹‘𝑔)〉} ∈ V → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ V) |
28 | 9, 25, 27 | 3syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ V) |
29 | | isset 2736 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ V ↔ ∃ℎ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) |
30 | 28, 29 | sylib 121 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃ℎ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) |
31 | 30 | 3ad2ant1 1013 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → ∃ℎ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) |
32 | | simpr3 1000 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑥 ∧ (𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) → ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) |
33 | | 19.8a 1583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉})) → ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) |
34 | | rspe 2519 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝑥 ∧ ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) → ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) |
35 | | tfrlemi1.3 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} |
36 | 35 | abeq2i 2281 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ ∈ 𝐵 ↔ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) |
37 | 34, 36 | sylibr 133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝑥 ∧ ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) → ℎ ∈ 𝐵) |
38 | 33, 37 | sylan2 284 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑥 ∧ (𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) → ℎ ∈ 𝐵) |
39 | 32, 38 | eqeltrrd 2248 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑥 ∧ (𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))) → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐵) |
40 | 39 | 3exp2 1220 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑥 → (𝑔 Fn 𝑧 → (𝑔 ∈ 𝐴 → (ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐵)))) |
41 | 40 | 3imp 1188 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴) → (ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐵)) |
42 | 41 | exlimdv 1812 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴) → (∃ℎ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐵)) |
43 | 24, 31, 42 | sylc 62 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐵) |
44 | | elunii 3801 |
. . . . . . . . . 10
⊢
((〈𝑧, (𝐹‘𝑔)〉 ∈ (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∧ (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐵) → 〈𝑧, (𝐹‘𝑔)〉 ∈ ∪
𝐵) |
45 | 13, 43, 44 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → 〈𝑧, (𝐹‘𝑔)〉 ∈ ∪
𝐵) |
46 | | opeq2 3766 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑔) → 〈𝑧, 𝑤〉 = 〈𝑧, (𝐹‘𝑔)〉) |
47 | 46 | eleq1d 2239 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐹‘𝑔) → (〈𝑧, 𝑤〉 ∈ ∪
𝐵 ↔ 〈𝑧, (𝐹‘𝑔)〉 ∈ ∪
𝐵)) |
48 | 47 | spcegv 2818 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑔) ∈ V → (〈𝑧, (𝐹‘𝑔)〉 ∈ ∪
𝐵 → ∃𝑤〈𝑧, 𝑤〉 ∈ ∪
𝐵)) |
49 | 7 | eldm2 4809 |
. . . . . . . . . 10
⊢ (𝑧 ∈ dom ∪ 𝐵
↔ ∃𝑤〈𝑧, 𝑤〉 ∈ ∪
𝐵) |
50 | 48, 49 | syl6ibr 161 |
. . . . . . . . 9
⊢ ((𝐹‘𝑔) ∈ V → (〈𝑧, (𝐹‘𝑔)〉 ∈ ∪
𝐵 → 𝑧 ∈ dom ∪
𝐵)) |
51 | 6, 45, 50 | sylc 62 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) → 𝑧 ∈ dom ∪
𝐵) |
52 | 51 | 3expia 1200 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥)) → ((𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → 𝑧 ∈ dom ∪
𝐵)) |
53 | 52 | exlimdv 1812 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ On ∧ 𝑧 ∈ 𝑥)) → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → 𝑧 ∈ dom ∪
𝐵)) |
54 | 53 | anassrs 398 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ On) ∧ 𝑧 ∈ 𝑥) → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → 𝑧 ∈ dom ∪
𝐵)) |
55 | 54 | ralimdva 2537 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ On) → (∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∀𝑧 ∈ 𝑥 𝑧 ∈ dom ∪
𝐵)) |
56 | 2, 55 | mpdan 419 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))) → ∀𝑧 ∈ 𝑥 𝑧 ∈ dom ∪
𝐵)) |
57 | 1, 56 | mpd 13 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝑥 𝑧 ∈ dom ∪
𝐵) |
58 | | dfss3 3137 |
. 2
⊢ (𝑥 ⊆ dom ∪ 𝐵
↔ ∀𝑧 ∈
𝑥 𝑧 ∈ dom ∪
𝐵) |
59 | 57, 58 | sylibr 133 |
1
⊢ (𝜑 → 𝑥 ⊆ dom ∪
𝐵) |