Step | Hyp | Ref
| Expression |
1 | | modelaxreplem.3 |
. . 3
⊢ (𝜓 → ∅ ∈ 𝑀) |
2 | | eleq1 2826 |
. . 3
⊢ (𝐴 = ∅ → (𝐴 ∈ 𝑀 ↔ ∅ ∈ 𝑀)) |
3 | 1, 2 | syl5ibrcom 247 |
. 2
⊢ (𝜓 → (𝐴 = ∅ → 𝐴 ∈ 𝑀)) |
4 | | vex 3481 |
. . . . . 6
⊢ 𝑥 ∈ V |
5 | | modelaxreplem1.5 |
. . . . . 6
⊢ 𝐴 ⊆ 𝑥 |
6 | 4, 5 | ssexi 5327 |
. . . . 5
⊢ 𝐴 ∈ V |
7 | 6 | 0sdom 9145 |
. . . 4
⊢ (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅) |
8 | | ssdomg 9038 |
. . . . . 6
⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥)) |
9 | 4, 5, 8 | mp2 9 |
. . . . 5
⊢ 𝐴 ≼ 𝑥 |
10 | | fodomr 9166 |
. . . . 5
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ 𝑥) → ∃𝑔 𝑔:𝑥–onto→𝐴) |
11 | 9, 10 | mpan2 691 |
. . . 4
⊢ (∅
≺ 𝐴 →
∃𝑔 𝑔:𝑥–onto→𝐴) |
12 | 7, 11 | sylbir 235 |
. . 3
⊢ (𝐴 ≠ ∅ →
∃𝑔 𝑔:𝑥–onto→𝐴) |
13 | | df-fo 6568 |
. . . . 5
⊢ (𝑔:𝑥–onto→𝐴 ↔ (𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴)) |
14 | | df-fn 6565 |
. . . . . . . 8
⊢ (𝑔 Fn 𝑥 ↔ (Fun 𝑔 ∧ dom 𝑔 = 𝑥)) |
15 | | modelaxreplem.4 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑥 ∈ 𝑀) |
16 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (dom
𝑔 = 𝑥 → (dom 𝑔 ∈ 𝑀 ↔ 𝑥 ∈ 𝑀)) |
17 | 15, 16 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ (𝜓 → (dom 𝑔 = 𝑥 → dom 𝑔 ∈ 𝑀)) |
18 | 17 | anim2d 612 |
. . . . . . . 8
⊢ (𝜓 → ((Fun 𝑔 ∧ dom 𝑔 = 𝑥) → (Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀))) |
19 | 14, 18 | biimtrid 242 |
. . . . . . 7
⊢ (𝜓 → (𝑔 Fn 𝑥 → (Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀))) |
20 | | modelaxreplem.1 |
. . . . . . . . 9
⊢ (𝜓 → 𝑥 ⊆ 𝑀) |
21 | 5, 20 | sstrid 4006 |
. . . . . . . 8
⊢ (𝜓 → 𝐴 ⊆ 𝑀) |
22 | | sseq1 4020 |
. . . . . . . 8
⊢ (ran
𝑔 = 𝐴 → (ran 𝑔 ⊆ 𝑀 ↔ 𝐴 ⊆ 𝑀)) |
23 | 21, 22 | syl5ibrcom 247 |
. . . . . . 7
⊢ (𝜓 → (ran 𝑔 = 𝐴 → ran 𝑔 ⊆ 𝑀)) |
24 | | df-3an 1088 |
. . . . . . . 8
⊢ ((Fun
𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀) ∧ ran 𝑔 ⊆ 𝑀)) |
25 | | modelaxreplem.2 |
. . . . . . . . 9
⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀)) |
26 | | funeq 6587 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔)) |
27 | | dmeq 5916 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔) |
28 | 27 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (dom 𝑓 ∈ 𝑀 ↔ dom 𝑔 ∈ 𝑀)) |
29 | | rneq 5949 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔) |
30 | 29 | sseq1d 4026 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (ran 𝑓 ⊆ 𝑀 ↔ ran 𝑔 ⊆ 𝑀)) |
31 | 26, 28, 30 | 3anbi123d 1435 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) ↔ (Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀))) |
32 | 29 | eleq1d 2823 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (ran 𝑓 ∈ 𝑀 ↔ ran 𝑔 ∈ 𝑀)) |
33 | 31, 32 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀))) |
34 | 33 | spvv 1993 |
. . . . . . . . 9
⊢
(∀𝑓((Fun
𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀) → ((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) |
35 | 25, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜓 → ((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) |
36 | 24, 35 | biimtrrid 243 |
. . . . . . 7
⊢ (𝜓 → (((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀) ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) |
37 | 19, 23, 36 | syl2and 608 |
. . . . . 6
⊢ (𝜓 → ((𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴) → ran 𝑔 ∈ 𝑀)) |
38 | | eleq1 2826 |
. . . . . . 7
⊢ (ran
𝑔 = 𝐴 → (ran 𝑔 ∈ 𝑀 ↔ 𝐴 ∈ 𝑀)) |
39 | 38 | adantl 481 |
. . . . . 6
⊢ ((𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴) → (ran 𝑔 ∈ 𝑀 ↔ 𝐴 ∈ 𝑀)) |
40 | 37, 39 | mpbidi 241 |
. . . . 5
⊢ (𝜓 → ((𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴) → 𝐴 ∈ 𝑀)) |
41 | 13, 40 | biimtrid 242 |
. . . 4
⊢ (𝜓 → (𝑔:𝑥–onto→𝐴 → 𝐴 ∈ 𝑀)) |
42 | 41 | exlimdv 1930 |
. . 3
⊢ (𝜓 → (∃𝑔 𝑔:𝑥–onto→𝐴 → 𝐴 ∈ 𝑀)) |
43 | 12, 42 | syl5 34 |
. 2
⊢ (𝜓 → (𝐴 ≠ ∅ → 𝐴 ∈ 𝑀)) |
44 | 3, 43 | pm2.61dne 3025 |
1
⊢ (𝜓 → 𝐴 ∈ 𝑀) |