Step |
Hyp |
Ref |
Expression |
1 |
|
infn0 |
⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ ) |
2 |
|
n0 |
⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 ) |
3 |
1 2
|
sylib |
⊢ ( ω ≼ 𝐴 → ∃ 𝑦 𝑦 ∈ 𝐴 ) |
4 |
|
reldom |
⊢ Rel ≼ |
5 |
4
|
brrelex2i |
⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V ) |
6 |
5
|
difexd |
⊢ ( ω ≼ 𝐴 → ( 𝐴 ∖ { 𝑦 } ) ∈ V ) |
7 |
6
|
adantr |
⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ V ) |
8 |
|
simpr |
⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) |
9 |
|
difsnpss |
⊢ ( 𝑦 ∈ 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ) |
10 |
8 9
|
sylib |
⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ) |
11 |
|
infdifsn |
⊢ ( ω ≼ 𝐴 → ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) |
12 |
11
|
adantr |
⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) |
13 |
10 12
|
jca |
⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ∧ ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) ) |
14 |
|
psseq1 |
⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝑥 ⊊ 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ) ) |
15 |
|
breq1 |
⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝑥 ≈ 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) ) |
16 |
14 15
|
anbi12d |
⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ↔ ( ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ∧ ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) ) ) |
17 |
7 13 16
|
spcedv |
⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) |
18 |
3 17
|
exlimddv |
⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) |