Proof of Theorem ismnu
Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . 6
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑙 = 𝑧) |
2 | 1 | pweqd 4552 |
. . . . 5
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧) |
3 | | simpl 483 |
. . . . 5
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑘 = 𝑈) |
4 | 2, 3 | sseq12d 3954 |
. . . 4
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (𝒫 𝑙 ⊆ 𝑘 ↔ 𝒫 𝑧 ⊆ 𝑈)) |
5 | 2 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧) |
6 | 5 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧) |
7 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤) |
8 | 6, 7 | sseq12d 3954 |
. . . . . . . 8
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙 ⊆ 𝑛 ↔ 𝒫 𝑧 ⊆ 𝑤)) |
9 | | simpl3 1192 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖) |
10 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣) |
11 | 9, 10 | eleq12d 2833 |
. . . . . . . . . . . . 13
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝 ∈ 𝑞 ↔ 𝑖 ∈ 𝑣)) |
12 | | simpl13 1249 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓) |
13 | 10, 12 | eleq12d 2833 |
. . . . . . . . . . . . 13
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞 ∈ 𝑚 ↔ 𝑣 ∈ 𝑓)) |
14 | 11, 13 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
15 | | simpl11 1247 |
. . . . . . . . . . . 12
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈) |
16 | 14, 15 | cbvrexdva2 3393 |
. . . . . . . . . . 11
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
17 | | simpl3 1192 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖) |
18 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢) |
19 | 17, 18 | eleq12d 2833 |
. . . . . . . . . . . . 13
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝 ∈ 𝑟 ↔ 𝑖 ∈ 𝑢)) |
20 | 18 | unieqd 4853 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ∪ 𝑟 = ∪
𝑢) |
21 | | simpl2 1191 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤) |
22 | 20, 21 | sseq12d 3954 |
. . . . . . . . . . . . 13
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (∪ 𝑟 ⊆ 𝑛 ↔ ∪ 𝑢 ⊆ 𝑤)) |
23 | 19, 22 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
24 | | simpl13 1249 |
. . . . . . . . . . . 12
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓) |
25 | 23, 24 | cbvrexdva2 3393 |
. . . . . . . . . . 11
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
26 | 16, 25 | imbi12d 345 |
. . . . . . . . . 10
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
27 | 26 | 3expa 1117 |
. . . . . . . . 9
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
28 | | simpll2 1212 |
. . . . . . . . 9
⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧) |
29 | 27, 28 | cbvraldva2 3392 |
. . . . . . . 8
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
30 | 8, 29 | anbi12d 631 |
. . . . . . 7
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |
31 | | simpl1 1190 |
. . . . . . 7
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈) |
32 | 30, 31 | cbvrexdva2 3393 |
. . . . . 6
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |
33 | 32 | 3expa 1117 |
. . . . 5
⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |
34 | 33 | cbvaldvaw 2041 |
. . . 4
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |
35 | 4, 34 | anbi12d 631 |
. . 3
⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → ((𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))) |
36 | 35, 3 | cbvraldva2 3392 |
. 2
⊢ (𝑘 = 𝑈 → (∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))) |
37 | | ismnu.1 |
. 2
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} |
38 | 36, 37 | elab2g 3611 |
1
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))) |