Step |
Hyp |
Ref |
Expression |
1 |
|
sdomdom |
⊢ ( 𝒫 𝑥 ≺ 𝐴 → 𝒫 𝑥 ≼ 𝐴 ) |
2 |
|
ondomen |
⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≼ 𝐴 ) → 𝒫 𝑥 ∈ dom card ) |
3 |
|
isnum2 |
⊢ ( 𝒫 𝑥 ∈ dom card ↔ ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 ) |
4 |
2 3
|
sylib |
⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≼ 𝐴 ) → ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 ) |
5 |
1 4
|
sylan2 |
⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 ) |
6 |
|
ensdomtr |
⊢ ( ( 𝑦 ≈ 𝒫 𝑥 ∧ 𝒫 𝑥 ≺ 𝐴 ) → 𝑦 ≺ 𝐴 ) |
7 |
6
|
ad2ant2l |
⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → 𝑦 ≺ 𝐴 ) |
8 |
|
sdomel |
⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑦 ≺ 𝐴 → 𝑦 ∈ 𝐴 ) ) |
9 |
8
|
ad2ant2r |
⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → ( 𝑦 ≺ 𝐴 → 𝑦 ∈ 𝐴 ) ) |
10 |
7 9
|
mpd |
⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → 𝑦 ∈ 𝐴 ) |
11 |
|
vex |
⊢ 𝑥 ∈ V |
12 |
11
|
canth2 |
⊢ 𝑥 ≺ 𝒫 𝑥 |
13 |
|
ensym |
⊢ ( 𝑦 ≈ 𝒫 𝑥 → 𝒫 𝑥 ≈ 𝑦 ) |
14 |
|
sdomentr |
⊢ ( ( 𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥 ≈ 𝑦 ) → 𝑥 ≺ 𝑦 ) |
15 |
12 13 14
|
sylancr |
⊢ ( 𝑦 ≈ 𝒫 𝑥 → 𝑥 ≺ 𝑦 ) |
16 |
15
|
ad2antlr |
⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → 𝑥 ≺ 𝑦 ) |
17 |
10 16
|
jca |
⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≺ 𝑦 ) ) |
18 |
17
|
expcom |
⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≺ 𝑦 ) ) ) |
19 |
18
|
reximdv2 |
⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ( ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) |
20 |
5 19
|
mpd |
⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) |
21 |
20
|
ex |
⊢ ( 𝐴 ∈ On → ( 𝒫 𝑥 ≺ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) |
22 |
21
|
ralimdv |
⊢ ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) |