Proof of Theorem modelaxreplem2
| Step | Hyp | Ref
| Expression |
| 1 | | modelaxreplem2.5 |
. . . 4
⊢
Ⅎ𝑤𝜓 |
| 2 | | modelaxreplem.1 |
. . . . . . 7
⊢ (𝜓 → 𝑥 ⊆ 𝑀) |
| 3 | 2 | sseld 3981 |
. . . . . 6
⊢ (𝜓 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑀)) |
| 4 | | modelaxreplem2.9 |
. . . . . . 7
⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦))) |
| 5 | | nfa1 2151 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑦𝜑 |
| 6 | 5 | rmo2i 3887 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃*𝑧 ∈ 𝑀 ∀𝑦𝜑) |
| 7 | | df-rmo 3379 |
. . . . . . . 8
⊢
(∃*𝑧 ∈
𝑀 ∀𝑦𝜑 ↔ ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) |
| 8 | 6, 7 | sylib 218 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) |
| 9 | 4, 8 | syl6 35 |
. . . . . 6
⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
| 10 | 3, 9 | syld 47 |
. . . . 5
⊢ (𝜓 → (𝑤 ∈ 𝑥 → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
| 11 | | moanimv 2618 |
. . . . 5
⊢
(∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) ↔ (𝑤 ∈ 𝑥 → ∃*𝑧(𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
| 12 | 10, 11 | sylibr 234 |
. . . 4
⊢ (𝜓 → ∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
| 13 | 1, 12 | alrimi 2213 |
. . 3
⊢ (𝜓 → ∀𝑤∃*𝑧(𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))) |
| 14 | | modelaxreplem2.8 |
. . . . 5
⊢ 𝐹 = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} |
| 15 | 14 | funeqi 6585 |
. . . 4
⊢ (Fun
𝐹 ↔ Fun {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}) |
| 16 | | funopab 6599 |
. . . 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 5913 |
. . . 4
⊢ dom 𝐹 = dom {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} |
| 23 | | dmopabss 5927 |
. . . 4
⊢ dom
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} ⊆ 𝑥 |
| 24 | 22, 23 | eqsstri 4029 |
. . 3
⊢ dom 𝐹 ⊆ 𝑥 |
| 25 | 2, 19, 20, 21, 24 | modelaxreplem1 44986 |
. 2
⊢ (𝜓 → dom 𝐹 ∈ 𝑀) |
| 26 | | an12 645 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑)) ↔ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) |
| 27 | 26 | opabbii 5208 |
. . . . . 6
⊢
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} = {〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} |
| 28 | 14, 27 | eqtri 2764 |
. . . . 5
⊢ 𝐹 = {〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} |
| 29 | 28 | rneqi 5946 |
. . . 4
⊢ ran 𝐹 = ran {〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} |
| 30 | | rnopabss 5964 |
. . . 4
⊢ ran
{〈𝑤, 𝑧〉 ∣ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))} ⊆ 𝑀 |
| 31 | 29, 30 | eqsstri 4029 |
. . 3
⊢ ran 𝐹 ⊆ 𝑀 |
| 32 | 31 | a1i 11 |
. 2
⊢ (𝜓 → ran 𝐹 ⊆ 𝑀) |
| 33 | | funex 7237 |
. . . 4
⊢ ((Fun
𝐹 ∧ dom 𝐹 ∈ 𝑀) → 𝐹 ∈ V) |
| 34 | 18, 25, 33 | syl2anc 584 |
. . 3
⊢ (𝜓 → 𝐹 ∈ V) |
| 35 | | funeq 6584 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (Fun 𝑓 ↔ Fun 𝐹)) |
| 36 | | dmeq 5912 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
| 37 | 36 | eleq1d 2825 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (dom 𝑓 ∈ 𝑀 ↔ dom 𝐹 ∈ 𝑀)) |
| 38 | | rneq 5945 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ran 𝑓 = ran 𝐹) |
| 39 | 38 | sseq1d 4014 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (ran 𝑓 ⊆ 𝑀 ↔ ran 𝐹 ⊆ 𝑀)) |
| 40 | 35, 37, 39 | 3anbi123d 1438 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) ↔ (Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀))) |
| 41 | 38 | eleq1d 2825 |
. . . . 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 1466 |
1
⊢ (𝜓 → ran 𝐹 ∈ 𝑀) |