Proof of Theorem modelaxreplem2
Step | Hyp | Ref
| Expression |
1 | | modelaxreplem2.5 |
. . . 4
⊢
Ⅎ𝑤𝜓 |
2 | | modelaxreplem.1 |
. . . . . . 7
⊢ (𝜓 → 𝑥 ⊆ 𝑀) |
3 | 2 | sseld 3993 |
. . . . . 6
⊢ (𝜓 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑀)) |
4 | | modelaxreplem2.9 |
. . . . . . 7
⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦))) |
5 | | nfa1 2148 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑦𝜑 |
6 | 5 | rmo2i 3896 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃*𝑧 ∈ 𝑀 ∀𝑦𝜑) |
7 | | df-rmo 3377 |
. . . . . . . 8
⊢
(∃*𝑧 ∈
𝑀 ∀𝑦𝜑 ↔ ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) |
8 | 6, 7 | sylib 218 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) |
9 | 4, 8 | syl6 35 |
. . . . . 6
⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
10 | 3, 9 | syld 47 |
. . . . 5
⊢ (𝜓 → (𝑤 ∈ 𝑥 → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
11 | | moanimv 2616 |
. . . . 5
⊢
(∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) ↔ (𝑤 ∈ 𝑥 → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
12 | 10, 11 | sylibr 234 |
. . . 4
⊢ (𝜓 → ∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
13 | 1, 12 | alrimi 2210 |
. . 3
⊢ (𝜓 → ∀𝑤∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
14 | | modelaxreplem2.8 |
. . . . 5
⊢ 𝐹 = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} |
15 | 14 | funeqi 6588 |
. . . 4
⊢ (Fun
𝐹 ↔ Fun {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}) |
16 | | funopab 6602 |
. . . 4
⊢ (Fun
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
17 | 15, 16 | bitri 275 |
. . 3
⊢ (Fun
𝐹 ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
18 | 13, 17 | sylibr 234 |
. 2
⊢ (𝜓 → Fun 𝐹) |
19 | | modelaxreplem.2 |
. . 3
⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀)) |
20 | | modelaxreplem.3 |
. . 3
⊢ (𝜓 → ∅ ∈ 𝑀) |
21 | | modelaxreplem.4 |
. . 3
⊢ (𝜓 → 𝑥 ∈ 𝑀) |
22 | 14 | dmeqi 5917 |
. . . 4
⊢ dom 𝐹 = dom {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} |
23 | | dmopabss 5931 |
. . . 4
⊢ dom
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} ⊆ 𝑥 |
24 | 22, 23 | eqsstri 4029 |
. . 3
⊢ dom 𝐹 ⊆ 𝑥 |
25 | 2, 19, 20, 21, 24 | modelaxreplem1 44942 |
. 2
⊢ (𝜓 → dom 𝐹 ∈ 𝑀) |
26 | | an12 645 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) ↔ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) |
27 | 26 | opabbii 5214 |
. . . . . 6
⊢
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} = {〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} |
28 | 14, 27 | eqtri 2762 |
. . . . 5
⊢ 𝐹 = {〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} |
29 | 28 | rneqi 5950 |
. . . 4
⊢ ran 𝐹 = ran {〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} |
30 | | rnopabss 5968 |
. . . 4
⊢ ran
{〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} ⊆ 𝑀 |
31 | 29, 30 | eqsstri 4029 |
. . 3
⊢ ran 𝐹 ⊆ 𝑀 |
32 | 31 | a1i 11 |
. 2
⊢ (𝜓 → ran 𝐹 ⊆ 𝑀) |
33 | | funex 7238 |
. . . 4
⊢ ((Fun
𝐹 ∧ dom 𝐹 ∈ 𝑀) → 𝐹 ∈ V) |
34 | 18, 25, 33 | syl2anc 584 |
. . 3
⊢ (𝜓 → 𝐹 ∈ V) |
35 | | funeq 6587 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (Fun 𝑓 ↔ Fun 𝐹)) |
36 | | dmeq 5916 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
37 | 36 | eleq1d 2823 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (dom 𝑓 ∈ 𝑀 ↔ dom 𝐹 ∈ 𝑀)) |
38 | | rneq 5949 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ran 𝑓 = ran 𝐹) |
39 | 38 | sseq1d 4026 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (ran 𝑓 ⊆ 𝑀 ↔ ran 𝐹 ⊆ 𝑀)) |
40 | 35, 37, 39 | 3anbi123d 1435 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) ↔ (Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀))) |
41 | 38 | eleq1d 2823 |
. . . . 5
⊢ (𝑓 = 𝐹 → (ran 𝑓 ∈ 𝑀 ↔ ran 𝐹 ∈ 𝑀)) |
42 | 40, 41 | imbi12d 344 |
. . . 4
⊢ (𝑓 = 𝐹 → (((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀) ↔ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀) → ran 𝐹 ∈ 𝑀))) |
43 | 42 | spcgv 3595 |
. . 3
⊢ (𝐹 ∈ V → (∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀) → ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀) → ran 𝐹 ∈ 𝑀))) |
44 | 34, 19, 43 | sylc 65 |
. 2
⊢ (𝜓 → ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀) → ran 𝐹 ∈ 𝑀)) |
45 | 18, 25, 32, 44 | mp3and 1463 |
1
⊢ (𝜓 → ran 𝐹 ∈ 𝑀) |