Proof of Theorem neicvgel1
Step | Hyp | Ref
| Expression |
1 | | neicvg.d |
. . . 4
⊢ 𝐷 = (𝑃‘𝐵) |
2 | | neicvg.h |
. . . 4
⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) |
3 | | neicvg.r |
. . . 4
⊢ (𝜑 → 𝑁𝐻𝑀) |
4 | 1, 2, 3 | neicvgbex 37430 |
. . 3
⊢ (𝜑 → 𝐵 ∈ V) |
5 | | neicvg.o |
. . . . . 6
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑𝑚 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) |
6 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐵 ∈ V) |
7 | | pwexg 4776 |
. . . . . . 7
⊢ (𝐵 ∈ V → 𝒫 𝐵 ∈ V) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝒫 𝐵 ∈ V) |
9 | | neicvg.f |
. . . . . 6
⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) |
10 | 5, 8, 6, 9 | fsovf1od 37330 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐹:(𝒫 𝐵 ↑𝑚 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑𝑚 𝐵)) |
11 | | f1ofn 6051 |
. . . . 5
⊢ (𝐹:(𝒫 𝐵 ↑𝑚 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑𝑚 𝐵) → 𝐹 Fn (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐹 Fn (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
13 | | neicvg.p |
. . . . . 6
⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) |
14 | 13, 1, 6 | dssmapf1od 37335 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐷:(𝒫 𝐵 ↑𝑚 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
15 | | f1of 6050 |
. . . . 5
⊢ (𝐷:(𝒫 𝐵 ↑𝑚 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝒫 𝐵) → 𝐷:(𝒫 𝐵 ↑𝑚 𝒫 𝐵)⟶(𝒫 𝐵 ↑𝑚
𝒫 𝐵)) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐷:(𝒫 𝐵 ↑𝑚 𝒫 𝐵)⟶(𝒫 𝐵 ↑𝑚
𝒫 𝐵)) |
17 | | neicvg.g |
. . . . 5
⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) |
18 | 5, 6, 8, 17 | fsovfd 37326 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐺:(𝒫 𝒫 𝐵 ↑𝑚 𝐵)⟶(𝒫 𝐵 ↑𝑚
𝒫 𝐵)) |
19 | 2 | breqi 4589 |
. . . . . 6
⊢ (𝑁𝐻𝑀 ↔ 𝑁(𝐹 ∘ (𝐷 ∘ 𝐺))𝑀) |
20 | 3, 19 | sylib 207 |
. . . . 5
⊢ (𝜑 → 𝑁(𝐹 ∘ (𝐷 ∘ 𝐺))𝑀) |
21 | 20 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝑁(𝐹 ∘ (𝐷 ∘ 𝐺))𝑀) |
22 | 12, 16, 18, 21 | brcofffn 37349 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ V) → (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) |
23 | 4, 22 | mpdan 699 |
. 2
⊢ (𝜑 → (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) |
24 | | simpr2 1061 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁))) |
25 | | neicvgel.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
26 | 25 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝑋 ∈ 𝐵) |
27 | | neicvgel.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) |
28 | 27 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝑆 ∈ 𝒫 𝐵) |
29 | 13, 1, 24, 26, 28 | ntrclselnel1 37375 |
. . 3
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑋 ∈ ((𝐺‘𝑁)‘𝑆) ↔ ¬ 𝑋 ∈ ((𝐷‘(𝐺‘𝑁))‘(𝐵 ∖ 𝑆)))) |
30 | | eqid 2610 |
. . . 4
⊢
(𝒫 𝐵𝑂𝐵) = (𝒫 𝐵𝑂𝐵) |
31 | | simpr1 1060 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝑁𝐺(𝐺‘𝑁)) |
32 | 17 | breqi 4589 |
. . . . . . 7
⊢ (𝑁𝐺(𝐺‘𝑁) ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁)) |
33 | 32 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑁𝐺(𝐺‘𝑁) ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁))) |
34 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝐵 ∈ V) |
35 | | id 22 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → 𝐵 ∈ V) |
36 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝐵𝑂𝒫 𝐵) = (𝐵𝑂𝒫 𝐵) |
37 | 5, 35, 7, 36 | fsovf1od 37330 |
. . . . . . . 8
⊢ (𝐵 ∈ V → (𝐵𝑂𝒫 𝐵):(𝒫 𝒫 𝐵 ↑𝑚 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
38 | 34, 37 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐵𝑂𝒫 𝐵):(𝒫 𝒫 𝐵 ↑𝑚 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
39 | | f1orel 6053 |
. . . . . . 7
⊢ ((𝐵𝑂𝒫 𝐵):(𝒫 𝒫 𝐵 ↑𝑚 𝐵)–1-1-onto→(𝒫 𝐵 ↑𝑚 𝒫 𝐵) → Rel (𝐵𝑂𝒫 𝐵)) |
40 | | relbrcnvg 5423 |
. . . . . . 7
⊢ (Rel
(𝐵𝑂𝒫 𝐵) → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁))) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁))) |
42 | 5, 35, 7, 36, 30 | fsovcnvd 37328 |
. . . . . . . 8
⊢ (𝐵 ∈ V → ◡(𝐵𝑂𝒫 𝐵) = (𝒫 𝐵𝑂𝐵)) |
43 | 42 | breqd 4594 |
. . . . . . 7
⊢ (𝐵 ∈ V → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁)) |
44 | 34, 43 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁)) |
45 | 33, 41, 44 | 3bitr2d 295 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑁𝐺(𝐺‘𝑁) ↔ (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁)) |
46 | 31, 45 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁) |
47 | 5, 30, 46, 26, 28 | ntrneiel 37399 |
. . 3
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑋 ∈ ((𝐺‘𝑁)‘𝑆) ↔ 𝑆 ∈ (𝑁‘𝑋))) |
48 | | simpr3 1062 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐷‘(𝐺‘𝑁))𝐹𝑀) |
49 | | difssd 3700 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∖ 𝑆) ⊆ 𝐵) |
50 | 4, 49 | sselpwd 4734 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) |
51 | 50 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) |
52 | 5, 9, 48, 26, 51 | ntrneiel 37399 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑋 ∈ ((𝐷‘(𝐺‘𝑁))‘(𝐵 ∖ 𝑆)) ↔ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |
53 | 52 | notbid 307 |
. . 3
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (¬ 𝑋 ∈ ((𝐷‘(𝐺‘𝑁))‘(𝐵 ∖ 𝑆)) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |
54 | 29, 47, 53 | 3bitr3d 297 |
. 2
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑆 ∈ (𝑁‘𝑋) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |
55 | 23, 54 | mpdan 699 |
1
⊢ (𝜑 → (𝑆 ∈ (𝑁‘𝑋) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |