Step |
Hyp |
Ref |
Expression |
1 |
|
cardf2 |
⊢ card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On |
2 |
|
ffun |
⊢ ( card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On → Fun card ) |
3 |
2
|
funfnd |
⊢ ( card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On → card Fn dom card ) |
4 |
1 3
|
ax-mp |
⊢ card Fn dom card |
5 |
|
fnimaeq0 |
⊢ ( ( card Fn dom card ∧ 𝐴 ⊆ dom card ) → ( ( card “ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) ) |
6 |
4 5
|
mpan |
⊢ ( 𝐴 ⊆ dom card → ( ( card “ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) ) |
7 |
6
|
necon3bid |
⊢ ( 𝐴 ⊆ dom card → ( ( card “ 𝐴 ) ≠ ∅ ↔ 𝐴 ≠ ∅ ) ) |
8 |
7
|
biimprd |
⊢ ( 𝐴 ⊆ dom card → ( 𝐴 ≠ ∅ → ( card “ 𝐴 ) ≠ ∅ ) ) |
9 |
8
|
imdistani |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) ) |
10 |
|
fimass |
⊢ ( card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On → ( card “ 𝐴 ) ⊆ On ) |
11 |
1 10
|
ax-mp |
⊢ ( card “ 𝐴 ) ⊆ On |
12 |
|
onssmin |
⊢ ( ( ( card “ 𝐴 ) ⊆ On ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ) |
13 |
11 12
|
mpan |
⊢ ( ( card “ 𝐴 ) ≠ ∅ → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ) |
14 |
|
ssel |
⊢ ( ( card “ 𝐴 ) ⊆ On → ( 𝑧 ∈ ( card “ 𝐴 ) → 𝑧 ∈ On ) ) |
15 |
|
ssel |
⊢ ( ( card “ 𝐴 ) ⊆ On → ( 𝑦 ∈ ( card “ 𝐴 ) → 𝑦 ∈ On ) ) |
16 |
14 15
|
anim12d |
⊢ ( ( card “ 𝐴 ) ⊆ On → ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ∈ On ∧ 𝑦 ∈ On ) ) ) |
17 |
11 16
|
ax-mp |
⊢ ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ∈ On ∧ 𝑦 ∈ On ) ) |
18 |
|
ontri1 |
⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑧 ) ) |
19 |
17 18
|
syl |
⊢ ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑧 ) ) |
20 |
|
epel |
⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 ) |
21 |
20
|
notbii |
⊢ ( ¬ 𝑦 E 𝑧 ↔ ¬ 𝑦 ∈ 𝑧 ) |
22 |
19 21
|
bitr4di |
⊢ ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) |
23 |
22
|
rgen2 |
⊢ ∀ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) |
24 |
|
r19.29r |
⊢ ( ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) ) |
25 |
13 23 24
|
sylancl |
⊢ ( ( card “ 𝐴 ) ≠ ∅ → ∃ 𝑧 ∈ ( card “ 𝐴 ) ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) ) |
26 |
|
r19.26 |
⊢ ( ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ∧ ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) ) |
27 |
|
bicom1 |
⊢ ( ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) → ( ¬ 𝑦 E 𝑧 ↔ 𝑧 ⊆ 𝑦 ) ) |
28 |
27
|
biimparc |
⊢ ( ( 𝑧 ⊆ 𝑦 ∧ ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ¬ 𝑦 E 𝑧 ) |
29 |
28
|
ralimi |
⊢ ( ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ∧ ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ) |
30 |
26 29
|
sylbir |
⊢ ( ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ) |
31 |
30
|
reximi |
⊢ ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ) |
32 |
25 31
|
syl |
⊢ ( ( card “ 𝐴 ) ≠ ∅ → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ) |
33 |
32
|
adantl |
⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ) |
34 |
|
breq2 |
⊢ ( 𝑧 = ( card ‘ 𝑥 ) → ( 𝑦 E 𝑧 ↔ 𝑦 E ( card ‘ 𝑥 ) ) ) |
35 |
34
|
notbid |
⊢ ( 𝑧 = ( card ‘ 𝑥 ) → ( ¬ 𝑦 E 𝑧 ↔ ¬ 𝑦 E ( card ‘ 𝑥 ) ) ) |
36 |
35
|
ralbidv |
⊢ ( 𝑧 = ( card ‘ 𝑥 ) → ( ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) ) |
37 |
36
|
rexima |
⊢ ( ( card Fn dom card ∧ 𝐴 ⊆ dom card ) → ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) ) |
38 |
4 37
|
mpan |
⊢ ( 𝐴 ⊆ dom card → ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) ) |
39 |
38
|
adantr |
⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) ) |
40 |
33 39
|
mpbid |
⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) |
41 |
|
fvex |
⊢ ( card ‘ 𝑥 ) ∈ V |
42 |
41
|
dfpred3 |
⊢ Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = { 𝑦 ∈ ( card “ 𝐴 ) ∣ 𝑦 E ( card ‘ 𝑥 ) } |
43 |
42
|
eqeq1i |
⊢ ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ { 𝑦 ∈ ( card “ 𝐴 ) ∣ 𝑦 E ( card ‘ 𝑥 ) } = ∅ ) |
44 |
|
rabeq0 |
⊢ ( { 𝑦 ∈ ( card “ 𝐴 ) ∣ 𝑦 E ( card ‘ 𝑥 ) } = ∅ ↔ ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) |
45 |
43 44
|
bitri |
⊢ ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) |
46 |
45
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) |
47 |
40 46
|
sylibr |
⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ) |
48 |
9 47
|
syl |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ) |
49 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom card ) |
50 |
|
cardpred |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) ) |
51 |
50
|
eqeq1d |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ) ) |
52 |
|
predss |
⊢ Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ 𝐴 |
53 |
|
sstr |
⊢ ( ( Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom card ) → Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ dom card ) |
54 |
52 53
|
mpan |
⊢ ( 𝐴 ⊆ dom card → Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ dom card ) |
55 |
|
fnimaeq0 |
⊢ ( ( card Fn dom card ∧ Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ dom card ) → ( ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) ) |
56 |
4 54 55
|
sylancr |
⊢ ( 𝐴 ⊆ dom card → ( ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) ) |
57 |
56
|
adantr |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → ( ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) ) |
58 |
51 57
|
bitrd |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) ) |
59 |
49 58
|
syldan |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ 𝐴 ) → ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) ) |
60 |
59
|
rexbidva |
⊢ ( 𝐴 ⊆ dom card → ( ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) ) |
61 |
60
|
adantr |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) ) |
62 |
48 61
|
mpbid |
⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) |