Proof of Theorem tfr1onlembxssdm
Step | Hyp | Ref
| Expression |
1 | | tfr1onlembacc.5 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) |
2 | | simp1 982 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 𝜑) |
3 | | simp2 983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 𝑧 ∈ 𝐷) |
4 | | tfr1onlembacc.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ 𝑋) |
5 | 2, 4 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 𝐷 ∈ 𝑋) |
6 | | tfr1on.x |
. . . . . . . . . . 11
⊢ (𝜑 → Ord 𝑋) |
7 | | ordtr1 4350 |
. . . . . . . . . . 11
⊢ (Ord
𝑋 → ((𝑧 ∈ 𝐷 ∧ 𝐷 ∈ 𝑋) → 𝑧 ∈ 𝑋)) |
8 | 6, 7 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ 𝐷 ∧ 𝐷 ∈ 𝑋) → 𝑧 ∈ 𝑋)) |
9 | 8 | imp 123 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝐷 ∈ 𝑋)) → 𝑧 ∈ 𝑋) |
10 | 2, 3, 5, 9 | syl12anc 1218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 𝑧 ∈ 𝑋) |
11 | | simp3l 1010 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 𝑔 Fn 𝑧) |
12 | | fneq2 5261 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑓 Fn 𝑥 ↔ 𝑓 Fn 𝑧)) |
13 | 12 | imbi1d 230 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ (𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V))) |
14 | 13 | albidv 1804 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ ∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V))) |
15 | | tfr1on.ex |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) |
16 | 15 | 3expia 1187 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V)) |
17 | 16 | alrimiv 1854 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V)) |
18 | 17 | ralrimiva 2530 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V)) |
19 | 18 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V)) |
20 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
21 | 14, 19, 20 | rspcdva 2821 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → ∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V)) |
22 | | fneq1 5260 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓 Fn 𝑧 ↔ 𝑔 Fn 𝑧)) |
23 | | fveq2 5470 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → (𝐺‘𝑓) = (𝐺‘𝑔)) |
24 | 23 | eleq1d 2226 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ((𝐺‘𝑓) ∈ V ↔ (𝐺‘𝑔) ∈ V)) |
25 | 22, 24 | imbi12d 233 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺‘𝑔) ∈ V))) |
26 | 25 | spv 1840 |
. . . . . . . . . 10
⊢
(∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V) → (𝑔 Fn 𝑧 → (𝐺‘𝑔) ∈ V)) |
27 | 21, 26 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑔 Fn 𝑧 → (𝐺‘𝑔) ∈ V)) |
28 | 27 | imp 123 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑋) ∧ 𝑔 Fn 𝑧) → (𝐺‘𝑔) ∈ V) |
29 | 2, 10, 11, 28 | syl21anc 1219 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → (𝐺‘𝑔) ∈ V) |
30 | | vex 2715 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
31 | | opexg 4190 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ V ∧ (𝐺‘𝑔) ∈ V) → 〈𝑧, (𝐺‘𝑔)〉 ∈ V) |
32 | 30, 29, 31 | sylancr 411 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 〈𝑧, (𝐺‘𝑔)〉 ∈ V) |
33 | | snidg 3590 |
. . . . . . . . 9
⊢
(〈𝑧, (𝐺‘𝑔)〉 ∈ V → 〈𝑧, (𝐺‘𝑔)〉 ∈ {〈𝑧, (𝐺‘𝑔)〉}) |
34 | | elun2 3276 |
. . . . . . . . 9
⊢
(〈𝑧, (𝐺‘𝑔)〉 ∈ {〈𝑧, (𝐺‘𝑔)〉} → 〈𝑧, (𝐺‘𝑔)〉 ∈ (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})) |
35 | 32, 33, 34 | 3syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 〈𝑧, (𝐺‘𝑔)〉 ∈ (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})) |
36 | | simp3r 1011 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))) |
37 | | rspe 2506 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑋 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → ∃𝑧 ∈ 𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) |
38 | 10, 11, 36, 37 | syl12anc 1218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → ∃𝑧 ∈ 𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) |
39 | | vex 2715 |
. . . . . . . . . . . 12
⊢ 𝑔 ∈ V |
40 | | tfr1onlemsucfn.1 |
. . . . . . . . . . . . 13
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} |
41 | 40 | tfr1onlem3ag 6286 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ V → (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ 𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))) |
42 | 39, 41 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ 𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) |
43 | 38, 42 | sylibr 133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 𝑔 ∈ 𝐴) |
44 | 3, 11, 43 | 3jca 1162 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → (𝑧 ∈ 𝐷 ∧ 𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴)) |
45 | | snexg 4147 |
. . . . . . . . . . 11
⊢
(〈𝑧, (𝐺‘𝑔)〉 ∈ V → {〈𝑧, (𝐺‘𝑔)〉} ∈ V) |
46 | | unexg 4405 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ V ∧ {〈𝑧, (𝐺‘𝑔)〉} ∈ V) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ V) |
47 | 39, 46 | mpan 421 |
. . . . . . . . . . 11
⊢
({〈𝑧, (𝐺‘𝑔)〉} ∈ V → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ V) |
48 | 32, 45, 47 | 3syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ V) |
49 | | isset 2718 |
. . . . . . . . . 10
⊢ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ V ↔ ∃ℎ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})) |
50 | 48, 49 | sylib 121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → ∃ℎ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})) |
51 | | simpr3 990 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) → ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})) |
52 | | 19.8a 1570 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})) → ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) |
53 | | rspe 2506 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) → ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) |
54 | | tfr1onlembacc.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} |
55 | 54 | abeq2i 2268 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ 𝐵 ↔ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) |
56 | 53, 55 | sylibr 133 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) → ℎ ∈ 𝐵) |
57 | 52, 56 | sylan2 284 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) → ℎ ∈ 𝐵) |
58 | 51, 57 | eqeltrrd 2235 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐵) |
59 | 58 | 3exp2 1207 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐷 → (𝑔 Fn 𝑧 → (𝑔 ∈ 𝐴 → (ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐵)))) |
60 | 59 | 3imp 1176 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐷 ∧ 𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴) → (ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐵)) |
61 | 60 | exlimdv 1799 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐷 ∧ 𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴) → (∃ℎ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐵)) |
62 | 44, 50, 61 | sylc 62 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐵) |
63 | | elunii 3779 |
. . . . . . . 8
⊢
((〈𝑧, (𝐺‘𝑔)〉 ∈ (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∧ (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐵) → 〈𝑧, (𝐺‘𝑔)〉 ∈ ∪
𝐵) |
64 | 35, 62, 63 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 〈𝑧, (𝐺‘𝑔)〉 ∈ ∪
𝐵) |
65 | | opeq2 3744 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐺‘𝑔) → 〈𝑧, 𝑤〉 = 〈𝑧, (𝐺‘𝑔)〉) |
66 | 65 | eleq1d 2226 |
. . . . . . . . 9
⊢ (𝑤 = (𝐺‘𝑔) → (〈𝑧, 𝑤〉 ∈ ∪
𝐵 ↔ 〈𝑧, (𝐺‘𝑔)〉 ∈ ∪
𝐵)) |
67 | 66 | spcegv 2800 |
. . . . . . . 8
⊢ ((𝐺‘𝑔) ∈ V → (〈𝑧, (𝐺‘𝑔)〉 ∈ ∪
𝐵 → ∃𝑤〈𝑧, 𝑤〉 ∈ ∪
𝐵)) |
68 | 30 | eldm2 4786 |
. . . . . . . 8
⊢ (𝑧 ∈ dom ∪ 𝐵
↔ ∃𝑤〈𝑧, 𝑤〉 ∈ ∪
𝐵) |
69 | 67, 68 | syl6ibr 161 |
. . . . . . 7
⊢ ((𝐺‘𝑔) ∈ V → (〈𝑧, (𝐺‘𝑔)〉 ∈ ∪
𝐵 → 𝑧 ∈ dom ∪
𝐵)) |
70 | 29, 64, 69 | sylc 62 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) → 𝑧 ∈ dom ∪
𝐵) |
71 | 70 | 3expia 1187 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ((𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))) → 𝑧 ∈ dom ∪
𝐵)) |
72 | 71 | exlimdv 1799 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))) → 𝑧 ∈ dom ∪
𝐵)) |
73 | 72 | ralimdva 2524 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))) → ∀𝑧 ∈ 𝐷 𝑧 ∈ dom ∪
𝐵)) |
74 | 1, 73 | mpd 13 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝐷 𝑧 ∈ dom ∪
𝐵) |
75 | | dfss3 3118 |
. 2
⊢ (𝐷 ⊆ dom ∪ 𝐵
↔ ∀𝑧 ∈
𝐷 𝑧 ∈ dom ∪
𝐵) |
76 | 74, 75 | sylibr 133 |
1
⊢ (𝜑 → 𝐷 ⊆ dom ∪
𝐵) |