Step | Hyp | Ref
| Expression |
1 | | ncfinraise 4481 |
. . . . . . . . 9
⊢ ((M ∈ Nn ∧ a ∈ M ∧ a ∈ M) → ∃n ∈ Nn (℘1a ∈ n ∧ ℘1a ∈ n)) |
2 | | anidm 625 |
. . . . . . . . . 10
⊢ ((℘1a ∈ n ∧ ℘1a ∈ n) ↔ ℘1a ∈ n) |
3 | 2 | rexbii 2639 |
. . . . . . . . 9
⊢ (∃n ∈ Nn (℘1a ∈ n ∧ ℘1a ∈ n) ↔ ∃n ∈ Nn ℘1a ∈ n) |
4 | 1, 3 | sylib 188 |
. . . . . . . 8
⊢ ((M ∈ Nn ∧ a ∈ M ∧ a ∈ M) → ∃n ∈ Nn ℘1a ∈ n) |
5 | 4 | 3anidm23 1241 |
. . . . . . 7
⊢ ((M ∈ Nn ∧ a ∈ M) → ∃n ∈ Nn ℘1a ∈ n) |
6 | 5 | ex 423 |
. . . . . 6
⊢ (M ∈ Nn → (a ∈ M →
∃n ∈ Nn ℘1a ∈ n)) |
7 | 6 | ancld 536 |
. . . . 5
⊢ (M ∈ Nn → (a ∈ M →
(a ∈
M ∧ ∃n ∈ Nn ℘1a ∈ n))) |
8 | 7 | eximdv 1622 |
. . . 4
⊢ (M ∈ Nn → (∃a a ∈ M →
∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n))) |
9 | 8 | imp 418 |
. . 3
⊢ ((M ∈ Nn ∧ ∃a a ∈ M) → ∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n)) |
10 | | n0 3559 |
. . . 4
⊢ (M ≠ ∅ ↔
∃a
a ∈
M) |
11 | 10 | anbi2i 675 |
. . 3
⊢ ((M ∈ Nn ∧ M ≠ ∅) ↔
(M ∈
Nn ∧ ∃a a ∈ M)) |
12 | | rexcom 2772 |
. . . 4
⊢ (∃n ∈ Nn ∃a ∈ M ℘1a ∈ n ↔ ∃a ∈ M ∃n ∈ Nn ℘1a ∈ n) |
13 | | df-rex 2620 |
. . . 4
⊢ (∃a ∈ M ∃n ∈ Nn ℘1a ∈ n ↔ ∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n)) |
14 | 12, 13 | bitri 240 |
. . 3
⊢ (∃n ∈ Nn ∃a ∈ M ℘1a ∈ n ↔ ∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n)) |
15 | 9, 11, 14 | 3imtr4i 257 |
. 2
⊢ ((M ∈ Nn ∧ M ≠ ∅) →
∃n ∈ Nn ∃a ∈ M ℘1a ∈ n) |
16 | | pw1eq 4143 |
. . . . . . . 8
⊢ (a = b →
℘1a = ℘1b) |
17 | 16 | eleq1d 2419 |
. . . . . . 7
⊢ (a = b →
(℘1a ∈ p ↔ ℘1b ∈ p)) |
18 | 17 | cbvrexv 2836 |
. . . . . 6
⊢ (∃a ∈ M ℘1a ∈ p ↔ ∃b ∈ M ℘1b ∈ p) |
19 | 18 | anbi2i 675 |
. . . . 5
⊢ ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) ↔ (∃a ∈ M ℘1a ∈ n ∧ ∃b ∈ M ℘1b ∈ p)) |
20 | | reeanv 2778 |
. . . . 5
⊢ (∃a ∈ M ∃b ∈ M (℘1a ∈ n ∧ ℘1b ∈ p) ↔ (∃a ∈ M ℘1a ∈ n ∧ ∃b ∈ M ℘1b ∈ p)) |
21 | 19, 20 | bitr4i 243 |
. . . 4
⊢ ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) ↔ ∃a ∈ M ∃b ∈ M (℘1a ∈ n ∧ ℘1b ∈ p)) |
22 | | simplll 734 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → M
∈ Nn
) |
23 | | simprll 738 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → a
∈ M) |
24 | | simprlr 739 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → b
∈ M) |
25 | | ncfinraise 4481 |
. . . . . . . 8
⊢ ((M ∈ Nn ∧ a ∈ M ∧ b ∈ M) → ∃q ∈ Nn (℘1a ∈ q ∧ ℘1b ∈ q)) |
26 | 22, 23, 24, 25 | syl3anc 1182 |
. . . . . . 7
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → ∃q ∈ Nn (℘1a ∈ q ∧ ℘1b ∈ q)) |
27 | | simp1rl 1020 |
. . . . . . . . . . . 12
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n
∈ Nn
) |
28 | | simp3l 983 |
. . . . . . . . . . . 12
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → q
∈ Nn
) |
29 | | simp2rl 1024 |
. . . . . . . . . . . 12
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1a ∈ n) |
30 | | simp3rl 1028 |
. . . . . . . . . . . 12
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1a ∈ q) |
31 | | nnceleq 4430 |
. . . . . . . . . . . 12
⊢ (((n ∈ Nn ∧ q ∈ Nn ) ∧ (℘1a ∈ n ∧ ℘1a ∈ q)) → n =
q) |
32 | 27, 28, 29, 30, 31 | syl22anc 1183 |
. . . . . . . . . . 11
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n =
q) |
33 | | simp1rr 1021 |
. . . . . . . . . . . 12
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → p
∈ Nn
) |
34 | | simp2rr 1025 |
. . . . . . . . . . . 12
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1b ∈ p) |
35 | | simp3rr 1029 |
. . . . . . . . . . . 12
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1b ∈ q) |
36 | | nnceleq 4430 |
. . . . . . . . . . . 12
⊢ (((p ∈ Nn ∧ q ∈ Nn ) ∧ (℘1b ∈ p ∧ ℘1b ∈ q)) → p =
q) |
37 | 33, 28, 34, 35, 36 | syl22anc 1183 |
. . . . . . . . . . 11
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → p =
q) |
38 | 32, 37 | eqtr4d 2388 |
. . . . . . . . . 10
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n =
p) |
39 | 38 | 3expa 1151 |
. . . . . . . . 9
⊢ (((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n =
p) |
40 | 39 | exp32 588 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → (q
∈ Nn →
((℘1a ∈ q ∧ ℘1b ∈ q) → n =
p))) |
41 | 40 | rexlimdv 2737 |
. . . . . . 7
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → (∃q ∈ Nn (℘1a ∈ q ∧ ℘1b ∈ q) → n =
p)) |
42 | 26, 41 | mpd 14 |
. . . . . 6
⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → n =
p) |
43 | 42 | exp32 588 |
. . . . 5
⊢ (((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) →
((a ∈
M ∧
b ∈
M) → ((℘1a ∈ n ∧ ℘1b ∈ p) → n =
p))) |
44 | 43 | rexlimdvv 2744 |
. . . 4
⊢ (((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) → (∃a ∈ M ∃b ∈ M (℘1a ∈ n ∧ ℘1b ∈ p) → n =
p)) |
45 | 21, 44 | syl5bi 208 |
. . 3
⊢ (((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) → ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) → n =
p)) |
46 | 45 | ralrimivva 2706 |
. 2
⊢ ((M ∈ Nn ∧ M ≠ ∅) →
∀n
∈ Nn ∀p ∈ Nn ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) → n =
p)) |
47 | | eleq2 2414 |
. . . 4
⊢ (n = p →
(℘1a ∈ n ↔ ℘1a ∈ p)) |
48 | 47 | rexbidv 2635 |
. . 3
⊢ (n = p →
(∃a
∈ M ℘1a ∈ n ↔ ∃a ∈ M ℘1a ∈ p)) |
49 | 48 | reu4 3030 |
. 2
⊢ (∃!n ∈ Nn ∃a ∈ M ℘1a ∈ n ↔ (∃n ∈ Nn ∃a ∈ M ℘1a ∈ n ∧ ∀n ∈ Nn ∀p ∈ Nn ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) → n =
p))) |
50 | 15, 46, 49 | sylanbrc 645 |
1
⊢ ((M ∈ Nn ∧ M ≠ ∅) →
∃!n
∈ Nn ∃a ∈ M ℘1a ∈ n) |