Step |
Hyp |
Ref |
Expression |
1 |
|
relsdom |
⊢ Rel ≺ |
2 |
1
|
brrelex2i |
⊢ ( ∅ ≺ 𝐴 → 𝐴 ∈ V ) |
3 |
|
reldom |
⊢ Rel ≼ |
4 |
3
|
brrelex2i |
⊢ ( 1o ≼ 𝐴 → 𝐴 ∈ V ) |
5 |
|
0sdomg |
⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
6 |
|
n0 |
⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) |
7 |
|
snssi |
⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ 𝐴 ) |
8 |
|
df1o2 |
⊢ 1o = { ∅ } |
9 |
|
0ex |
⊢ ∅ ∈ V |
10 |
|
vex |
⊢ 𝑥 ∈ V |
11 |
|
en2sn |
⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → { ∅ } ≈ { 𝑥 } ) |
12 |
9 10 11
|
mp2an |
⊢ { ∅ } ≈ { 𝑥 } |
13 |
8 12
|
eqbrtri |
⊢ 1o ≈ { 𝑥 } |
14 |
|
endom |
⊢ ( 1o ≈ { 𝑥 } → 1o ≼ { 𝑥 } ) |
15 |
13 14
|
ax-mp |
⊢ 1o ≼ { 𝑥 } |
16 |
|
domssr |
⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 } ⊆ 𝐴 ∧ 1o ≼ { 𝑥 } ) → 1o ≼ 𝐴 ) |
17 |
15 16
|
mp3an3 |
⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 } ⊆ 𝐴 ) → 1o ≼ 𝐴 ) |
18 |
17
|
ex |
⊢ ( 𝐴 ∈ V → ( { 𝑥 } ⊆ 𝐴 → 1o ≼ 𝐴 ) ) |
19 |
7 18
|
syl5 |
⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 → 1o ≼ 𝐴 ) ) |
20 |
19
|
exlimdv |
⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 𝑥 ∈ 𝐴 → 1o ≼ 𝐴 ) ) |
21 |
6 20
|
biimtrid |
⊢ ( 𝐴 ∈ V → ( 𝐴 ≠ ∅ → 1o ≼ 𝐴 ) ) |
22 |
|
1n0 |
⊢ 1o ≠ ∅ |
23 |
|
dom0 |
⊢ ( 1o ≼ ∅ ↔ 1o = ∅ ) |
24 |
22 23
|
nemtbir |
⊢ ¬ 1o ≼ ∅ |
25 |
|
breq2 |
⊢ ( 𝐴 = ∅ → ( 1o ≼ 𝐴 ↔ 1o ≼ ∅ ) ) |
26 |
24 25
|
mtbiri |
⊢ ( 𝐴 = ∅ → ¬ 1o ≼ 𝐴 ) |
27 |
26
|
necon2ai |
⊢ ( 1o ≼ 𝐴 → 𝐴 ≠ ∅ ) |
28 |
21 27
|
impbid1 |
⊢ ( 𝐴 ∈ V → ( 𝐴 ≠ ∅ ↔ 1o ≼ 𝐴 ) ) |
29 |
5 28
|
bitrd |
⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 1o ≼ 𝐴 ) ) |
30 |
2 4 29
|
pm5.21nii |
⊢ ( ∅ ≺ 𝐴 ↔ 1o ≼ 𝐴 ) |