| Step |
Hyp |
Ref |
Expression |
| 1 |
|
modelaxreplem.1 |
⊢ ( 𝜓 → 𝑥 ⊆ 𝑀 ) |
| 2 |
|
modelaxreplem.2 |
⊢ ( 𝜓 → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ) |
| 3 |
|
modelaxreplem.3 |
⊢ ( 𝜓 → ∅ ∈ 𝑀 ) |
| 4 |
|
modelaxreplem.4 |
⊢ ( 𝜓 → 𝑥 ∈ 𝑀 ) |
| 5 |
|
modelaxreplem1.5 |
⊢ 𝐴 ⊆ 𝑥 |
| 6 |
|
eleq1 |
⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ 𝑀 ↔ ∅ ∈ 𝑀 ) ) |
| 7 |
3 6
|
syl5ibrcom |
⊢ ( 𝜓 → ( 𝐴 = ∅ → 𝐴 ∈ 𝑀 ) ) |
| 8 |
|
vex |
⊢ 𝑥 ∈ V |
| 9 |
8 5
|
ssexi |
⊢ 𝐴 ∈ V |
| 10 |
9
|
0sdom |
⊢ ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) |
| 11 |
|
ssdomg |
⊢ ( 𝑥 ∈ V → ( 𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥 ) ) |
| 12 |
8 5 11
|
mp2 |
⊢ 𝐴 ≼ 𝑥 |
| 13 |
|
fodomr |
⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ 𝑥 ) → ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 ) |
| 14 |
12 13
|
mpan2 |
⊢ ( ∅ ≺ 𝐴 → ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 ) |
| 15 |
10 14
|
sylbir |
⊢ ( 𝐴 ≠ ∅ → ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 ) |
| 16 |
|
df-fo |
⊢ ( 𝑔 : 𝑥 –onto→ 𝐴 ↔ ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) ) |
| 17 |
|
df-fn |
⊢ ( 𝑔 Fn 𝑥 ↔ ( Fun 𝑔 ∧ dom 𝑔 = 𝑥 ) ) |
| 18 |
|
eleq1 |
⊢ ( dom 𝑔 = 𝑥 → ( dom 𝑔 ∈ 𝑀 ↔ 𝑥 ∈ 𝑀 ) ) |
| 19 |
4 18
|
syl5ibrcom |
⊢ ( 𝜓 → ( dom 𝑔 = 𝑥 → dom 𝑔 ∈ 𝑀 ) ) |
| 20 |
19
|
anim2d |
⊢ ( 𝜓 → ( ( Fun 𝑔 ∧ dom 𝑔 = 𝑥 ) → ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ) ) |
| 21 |
17 20
|
biimtrid |
⊢ ( 𝜓 → ( 𝑔 Fn 𝑥 → ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ) ) |
| 22 |
5 1
|
sstrid |
⊢ ( 𝜓 → 𝐴 ⊆ 𝑀 ) |
| 23 |
|
sseq1 |
⊢ ( ran 𝑔 = 𝐴 → ( ran 𝑔 ⊆ 𝑀 ↔ 𝐴 ⊆ 𝑀 ) ) |
| 24 |
22 23
|
syl5ibrcom |
⊢ ( 𝜓 → ( ran 𝑔 = 𝐴 → ran 𝑔 ⊆ 𝑀 ) ) |
| 25 |
|
df-3an |
⊢ ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) ↔ ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ∧ ran 𝑔 ⊆ 𝑀 ) ) |
| 26 |
|
funeq |
⊢ ( 𝑓 = 𝑔 → ( Fun 𝑓 ↔ Fun 𝑔 ) ) |
| 27 |
|
dmeq |
⊢ ( 𝑓 = 𝑔 → dom 𝑓 = dom 𝑔 ) |
| 28 |
27
|
eleq1d |
⊢ ( 𝑓 = 𝑔 → ( dom 𝑓 ∈ 𝑀 ↔ dom 𝑔 ∈ 𝑀 ) ) |
| 29 |
|
rneq |
⊢ ( 𝑓 = 𝑔 → ran 𝑓 = ran 𝑔 ) |
| 30 |
29
|
sseq1d |
⊢ ( 𝑓 = 𝑔 → ( ran 𝑓 ⊆ 𝑀 ↔ ran 𝑔 ⊆ 𝑀 ) ) |
| 31 |
26 28 30
|
3anbi123d |
⊢ ( 𝑓 = 𝑔 → ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) ↔ ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) ) ) |
| 32 |
29
|
eleq1d |
⊢ ( 𝑓 = 𝑔 → ( ran 𝑓 ∈ 𝑀 ↔ ran 𝑔 ∈ 𝑀 ) ) |
| 33 |
31 32
|
imbi12d |
⊢ ( 𝑓 = 𝑔 → ( ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ↔ ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ) |
| 34 |
33
|
spvv |
⊢ ( ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) → ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) |
| 35 |
2 34
|
syl |
⊢ ( 𝜓 → ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) |
| 36 |
25 35
|
biimtrrid |
⊢ ( 𝜓 → ( ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) |
| 37 |
21 24 36
|
syl2and |
⊢ ( 𝜓 → ( ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) → ran 𝑔 ∈ 𝑀 ) ) |
| 38 |
|
eleq1 |
⊢ ( ran 𝑔 = 𝐴 → ( ran 𝑔 ∈ 𝑀 ↔ 𝐴 ∈ 𝑀 ) ) |
| 39 |
38
|
adantl |
⊢ ( ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) → ( ran 𝑔 ∈ 𝑀 ↔ 𝐴 ∈ 𝑀 ) ) |
| 40 |
37 39
|
mpbidi |
⊢ ( 𝜓 → ( ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) → 𝐴 ∈ 𝑀 ) ) |
| 41 |
16 40
|
biimtrid |
⊢ ( 𝜓 → ( 𝑔 : 𝑥 –onto→ 𝐴 → 𝐴 ∈ 𝑀 ) ) |
| 42 |
41
|
exlimdv |
⊢ ( 𝜓 → ( ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 → 𝐴 ∈ 𝑀 ) ) |
| 43 |
15 42
|
syl5 |
⊢ ( 𝜓 → ( 𝐴 ≠ ∅ → 𝐴 ∈ 𝑀 ) ) |
| 44 |
7 43
|
pm2.61dne |
⊢ ( 𝜓 → 𝐴 ∈ 𝑀 ) |