Step | Hyp | Ref
| Expression |
1 | | cardf2 9390 |
. . . . . . . 8
⊢
card:{𝑧 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑧}⟶On |
2 | | ffun 6494 |
. . . . . . . . 9
⊢
(card:{𝑧 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑧}⟶On → Fun card) |
3 | 2 | funfnd 6359 |
. . . . . . . 8
⊢
(card:{𝑧 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑧}⟶On → card Fn dom
card) |
4 | 1, 3 | ax-mp 5 |
. . . . . . 7
⊢ card Fn
dom card |
5 | | fnimaeq0 6457 |
. . . . . . 7
⊢ ((card Fn
dom card ∧ 𝐴 ⊆
dom card) → ((card “ 𝐴) = ∅ ↔ 𝐴 = ∅)) |
6 | 4, 5 | mpan 690 |
. . . . . 6
⊢ (𝐴 ⊆ dom card → ((card
“ 𝐴) = ∅ ↔
𝐴 =
∅)) |
7 | 6 | necon3bid 2993 |
. . . . 5
⊢ (𝐴 ⊆ dom card → ((card
“ 𝐴) ≠ ∅
↔ 𝐴 ≠
∅)) |
8 | 7 | biimprd 251 |
. . . 4
⊢ (𝐴 ⊆ dom card → (𝐴 ≠ ∅ → (card
“ 𝐴) ≠
∅)) |
9 | 8 | imdistani 573 |
. . 3
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) → (𝐴 ⊆ dom card ∧ (card
“ 𝐴) ≠
∅)) |
10 | | fimass 6533 |
. . . . . . . . . 10
⊢
(card:{𝑧 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑧}⟶On → (card “ 𝐴) ⊆ On) |
11 | 1, 10 | ax-mp 5 |
. . . . . . . . 9
⊢ (card
“ 𝐴) ⊆
On |
12 | | onssmin 7504 |
. . . . . . . . 9
⊢ (((card
“ 𝐴) ⊆ On ∧
(card “ 𝐴) ≠
∅) → ∃𝑧
∈ (card “ 𝐴)∀𝑦 ∈ (card “ 𝐴)𝑧 ⊆ 𝑦) |
13 | 11, 12 | mpan 690 |
. . . . . . . 8
⊢ ((card
“ 𝐴) ≠ ∅
→ ∃𝑧 ∈
(card “ 𝐴)∀𝑦 ∈ (card “ 𝐴)𝑧 ⊆ 𝑦) |
14 | | ssel 3881 |
. . . . . . . . . . . . 13
⊢ ((card
“ 𝐴) ⊆ On
→ (𝑧 ∈ (card
“ 𝐴) → 𝑧 ∈ On)) |
15 | | ssel 3881 |
. . . . . . . . . . . . 13
⊢ ((card
“ 𝐴) ⊆ On
→ (𝑦 ∈ (card
“ 𝐴) → 𝑦 ∈ On)) |
16 | 14, 15 | anim12d 612 |
. . . . . . . . . . . 12
⊢ ((card
“ 𝐴) ⊆ On
→ ((𝑧 ∈ (card
“ 𝐴) ∧ 𝑦 ∈ (card “ 𝐴)) → (𝑧 ∈ On ∧ 𝑦 ∈ On))) |
17 | 11, 16 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (card “ 𝐴) ∧ 𝑦 ∈ (card “ 𝐴)) → (𝑧 ∈ On ∧ 𝑦 ∈ On)) |
18 | | ontri1 6196 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ On) → (𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑧)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (card “ 𝐴) ∧ 𝑦 ∈ (card “ 𝐴)) → (𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑧)) |
20 | | epel 5431 |
. . . . . . . . . . 11
⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧) |
21 | 20 | notbii 324 |
. . . . . . . . . 10
⊢ (¬
𝑦 E 𝑧 ↔ ¬ 𝑦 ∈ 𝑧) |
22 | 19, 21 | bitr4di 293 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (card “ 𝐴) ∧ 𝑦 ∈ (card “ 𝐴)) → (𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧)) |
23 | 22 | rgen2 3130 |
. . . . . . . 8
⊢
∀𝑧 ∈
(card “ 𝐴)∀𝑦 ∈ (card “ 𝐴)(𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧) |
24 | | r19.29r 3180 |
. . . . . . . 8
⊢
((∃𝑧 ∈
(card “ 𝐴)∀𝑦 ∈ (card “ 𝐴)𝑧 ⊆ 𝑦 ∧ ∀𝑧 ∈ (card “ 𝐴)∀𝑦 ∈ (card “ 𝐴)(𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧)) → ∃𝑧 ∈ (card “ 𝐴)(∀𝑦 ∈ (card “ 𝐴)𝑧 ⊆ 𝑦 ∧ ∀𝑦 ∈ (card “ 𝐴)(𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧))) |
25 | 13, 23, 24 | sylancl 590 |
. . . . . . 7
⊢ ((card
“ 𝐴) ≠ ∅
→ ∃𝑧 ∈
(card “ 𝐴)(∀𝑦 ∈ (card “ 𝐴)𝑧 ⊆ 𝑦 ∧ ∀𝑦 ∈ (card “ 𝐴)(𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧))) |
26 | | r19.26 3099 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
(card “ 𝐴)(𝑧 ⊆ 𝑦 ∧ (𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧)) ↔ (∀𝑦 ∈ (card “ 𝐴)𝑧 ⊆ 𝑦 ∧ ∀𝑦 ∈ (card “ 𝐴)(𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧))) |
27 | | bicom1 224 |
. . . . . . . . . . 11
⊢ ((𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧) → (¬ 𝑦 E 𝑧 ↔ 𝑧 ⊆ 𝑦)) |
28 | 27 | biimparc 484 |
. . . . . . . . . 10
⊢ ((𝑧 ⊆ 𝑦 ∧ (𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧)) → ¬ 𝑦 E 𝑧) |
29 | 28 | ralimi 3090 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
(card “ 𝐴)(𝑧 ⊆ 𝑦 ∧ (𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧)) → ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧) |
30 | 26, 29 | sylbir 238 |
. . . . . . . 8
⊢
((∀𝑦 ∈
(card “ 𝐴)𝑧 ⊆ 𝑦 ∧ ∀𝑦 ∈ (card “ 𝐴)(𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧)) → ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧) |
31 | 30 | reximi 3169 |
. . . . . . 7
⊢
(∃𝑧 ∈
(card “ 𝐴)(∀𝑦 ∈ (card “ 𝐴)𝑧 ⊆ 𝑦 ∧ ∀𝑦 ∈ (card “ 𝐴)(𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧)) → ∃𝑧 ∈ (card “ 𝐴)∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧) |
32 | 25, 31 | syl 17 |
. . . . . 6
⊢ ((card
“ 𝐴) ≠ ∅
→ ∃𝑧 ∈
(card “ 𝐴)∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧) |
33 | 32 | adantl 486 |
. . . . 5
⊢ ((𝐴 ⊆ dom card ∧ (card
“ 𝐴) ≠ ∅)
→ ∃𝑧 ∈
(card “ 𝐴)∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧) |
34 | | breq2 5029 |
. . . . . . . . . 10
⊢ (𝑧 = (card‘𝑥) → (𝑦 E 𝑧 ↔ 𝑦 E (card‘𝑥))) |
35 | 34 | notbid 322 |
. . . . . . . . 9
⊢ (𝑧 = (card‘𝑥) → (¬ 𝑦 E 𝑧 ↔ ¬ 𝑦 E (card‘𝑥))) |
36 | 35 | ralbidv 3124 |
. . . . . . . 8
⊢ (𝑧 = (card‘𝑥) → (∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧 ↔ ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E (card‘𝑥))) |
37 | 36 | rexima 6984 |
. . . . . . 7
⊢ ((card Fn
dom card ∧ 𝐴 ⊆
dom card) → (∃𝑧
∈ (card “ 𝐴)∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E (card‘𝑥))) |
38 | 4, 37 | mpan 690 |
. . . . . 6
⊢ (𝐴 ⊆ dom card →
(∃𝑧 ∈ (card
“ 𝐴)∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E (card‘𝑥))) |
39 | 38 | adantr 485 |
. . . . 5
⊢ ((𝐴 ⊆ dom card ∧ (card
“ 𝐴) ≠ ∅)
→ (∃𝑧 ∈
(card “ 𝐴)∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E 𝑧 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E (card‘𝑥))) |
40 | 33, 39 | mpbid 235 |
. . . 4
⊢ ((𝐴 ⊆ dom card ∧ (card
“ 𝐴) ≠ ∅)
→ ∃𝑥 ∈
𝐴 ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E (card‘𝑥)) |
41 | | fvex 6664 |
. . . . . . . 8
⊢
(card‘𝑥)
∈ V |
42 | 41 | dfpred3 6129 |
. . . . . . 7
⊢ Pred( E ,
(card “ 𝐴),
(card‘𝑥)) = {𝑦 ∈ (card “ 𝐴) ∣ 𝑦 E (card‘𝑥)} |
43 | 42 | eqeq1i 2764 |
. . . . . 6
⊢ (Pred( E
, (card “ 𝐴),
(card‘𝑥)) = ∅
↔ {𝑦 ∈ (card
“ 𝐴) ∣ 𝑦 E (card‘𝑥)} = ∅) |
44 | | rabeq0 4274 |
. . . . . 6
⊢ ({𝑦 ∈ (card “ 𝐴) ∣ 𝑦 E (card‘𝑥)} = ∅ ↔ ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E (card‘𝑥)) |
45 | 43, 44 | bitri 278 |
. . . . 5
⊢ (Pred( E
, (card “ 𝐴),
(card‘𝑥)) = ∅
↔ ∀𝑦 ∈
(card “ 𝐴) ¬
𝑦 E (card‘𝑥)) |
46 | 45 | rexbii 3173 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 Pred( E , (card “
𝐴), (card‘𝑥)) = ∅ ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ (card “ 𝐴) ¬ 𝑦 E (card‘𝑥)) |
47 | 40, 46 | sylibr 237 |
. . 3
⊢ ((𝐴 ⊆ dom card ∧ (card
“ 𝐴) ≠ ∅)
→ ∃𝑥 ∈
𝐴 Pred( E , (card “
𝐴), (card‘𝑥)) = ∅) |
48 | 9, 47 | syl 17 |
. 2
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ 𝐴 Pred( E , (card “ 𝐴), (card‘𝑥)) = ∅) |
49 | | ssel2 3883 |
. . . . 5
⊢ ((𝐴 ⊆ dom card ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom card) |
50 | | cardpred 32576 |
. . . . . . 7
⊢ ((𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card) → Pred( E
, (card “ 𝐴),
(card‘𝑥)) = (card
“ Pred( ≺ , 𝐴,
𝑥))) |
51 | 50 | eqeq1d 2761 |
. . . . . 6
⊢ ((𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card) → (Pred(
E , (card “ 𝐴),
(card‘𝑥)) = ∅
↔ (card “ Pred( ≺ , 𝐴, 𝑥)) = ∅)) |
52 | | predss 6126 |
. . . . . . . . 9
⊢ Pred(
≺ , 𝐴, 𝑥) ⊆ 𝐴 |
53 | | sstr 3896 |
. . . . . . . . 9
⊢ ((Pred(
≺ , 𝐴, 𝑥) ⊆ 𝐴 ∧ 𝐴 ⊆ dom card) → Pred( ≺ ,
𝐴, 𝑥) ⊆ dom card) |
54 | 52, 53 | mpan 690 |
. . . . . . . 8
⊢ (𝐴 ⊆ dom card → Pred(
≺ , 𝐴, 𝑥) ⊆ dom
card) |
55 | | fnimaeq0 6457 |
. . . . . . . 8
⊢ ((card Fn
dom card ∧ Pred( ≺ , 𝐴, 𝑥) ⊆ dom card) → ((card “
Pred( ≺ , 𝐴, 𝑥)) = ∅ ↔ Pred(
≺ , 𝐴, 𝑥) = ∅)) |
56 | 4, 54, 55 | sylancr 591 |
. . . . . . 7
⊢ (𝐴 ⊆ dom card → ((card
“ Pred( ≺ , 𝐴,
𝑥)) = ∅ ↔ Pred(
≺ , 𝐴, 𝑥) = ∅)) |
57 | 56 | adantr 485 |
. . . . . 6
⊢ ((𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card) → ((card
“ Pred( ≺ , 𝐴,
𝑥)) = ∅ ↔ Pred(
≺ , 𝐴, 𝑥) = ∅)) |
58 | 51, 57 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card) → (Pred(
E , (card “ 𝐴),
(card‘𝑥)) = ∅
↔ Pred( ≺ , 𝐴,
𝑥) =
∅)) |
59 | 49, 58 | syldan 595 |
. . . 4
⊢ ((𝐴 ⊆ dom card ∧ 𝑥 ∈ 𝐴) → (Pred( E , (card “ 𝐴), (card‘𝑥)) = ∅ ↔ Pred(
≺ , 𝐴, 𝑥) = ∅)) |
60 | 59 | rexbidva 3218 |
. . 3
⊢ (𝐴 ⊆ dom card →
(∃𝑥 ∈ 𝐴 Pred( E , (card “ 𝐴), (card‘𝑥)) = ∅ ↔ ∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅)) |
61 | 60 | adantr 485 |
. 2
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ 𝐴 Pred( E , (card “ 𝐴), (card‘𝑥)) = ∅ ↔ ∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅)) |
62 | 48, 61 | mpbid 235 |
1
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅) |