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 41722 |
. . 3
⊢ (𝜑 → 𝐵 ∈ V) |
5 | | neicvg.o |
. . . . . 6
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) |
6 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐵 ∈ V) |
7 | 6 | pwexd 5302 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝒫 𝐵 ∈ V) |
8 | | neicvg.f |
. . . . . 6
⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) |
9 | 5, 7, 6, 8 | fsovf1od 41624 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐹:(𝒫 𝐵 ↑m 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑m 𝐵)) |
10 | | f1ofn 6717 |
. . . . 5
⊢ (𝐹:(𝒫 𝐵 ↑m 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑m 𝐵) → 𝐹 Fn (𝒫 𝐵 ↑m 𝒫 𝐵)) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐹 Fn (𝒫 𝐵 ↑m 𝒫 𝐵)) |
12 | | neicvg.p |
. . . . . 6
⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) |
13 | 12, 1, 6 | dssmapf1od 41629 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐷:(𝒫 𝐵 ↑m 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝒫 𝐵)) |
14 | | f1of 6716 |
. . . . 5
⊢ (𝐷:(𝒫 𝐵 ↑m 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝒫 𝐵) → 𝐷:(𝒫 𝐵 ↑m 𝒫 𝐵)⟶(𝒫 𝐵 ↑m 𝒫
𝐵)) |
15 | 13, 14 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐷:(𝒫 𝐵 ↑m 𝒫 𝐵)⟶(𝒫 𝐵 ↑m 𝒫
𝐵)) |
16 | | neicvg.g |
. . . . 5
⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) |
17 | 5, 6, 7, 16 | fsovfd 41620 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝐺:(𝒫 𝒫 𝐵 ↑m 𝐵)⟶(𝒫 𝐵 ↑m 𝒫 𝐵)) |
18 | 2 | breqi 5080 |
. . . . . 6
⊢ (𝑁𝐻𝑀 ↔ 𝑁(𝐹 ∘ (𝐷 ∘ 𝐺))𝑀) |
19 | 3, 18 | sylib 217 |
. . . . 5
⊢ (𝜑 → 𝑁(𝐹 ∘ (𝐷 ∘ 𝐺))𝑀) |
20 | 19 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ V) → 𝑁(𝐹 ∘ (𝐷 ∘ 𝐺))𝑀) |
21 | 11, 15, 17, 20 | brcofffn 41641 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ V) → (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) |
22 | 4, 21 | mpdan 684 |
. 2
⊢ (𝜑 → (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) |
23 | | simpr2 1194 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁))) |
24 | | neicvgel.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
25 | 24 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝑋 ∈ 𝐵) |
26 | | neicvgel.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) |
27 | 26 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝑆 ∈ 𝒫 𝐵) |
28 | 12, 1, 23, 25, 27 | ntrclselnel1 41667 |
. . 3
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑋 ∈ ((𝐺‘𝑁)‘𝑆) ↔ ¬ 𝑋 ∈ ((𝐷‘(𝐺‘𝑁))‘(𝐵 ∖ 𝑆)))) |
29 | | eqid 2738 |
. . . 4
⊢
(𝒫 𝐵𝑂𝐵) = (𝒫 𝐵𝑂𝐵) |
30 | | simpr1 1193 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝑁𝐺(𝐺‘𝑁)) |
31 | 16 | breqi 5080 |
. . . . . . 7
⊢ (𝑁𝐺(𝐺‘𝑁) ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁)) |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑁𝐺(𝐺‘𝑁) ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁))) |
33 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → 𝐵 ∈ V) |
34 | | id 22 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → 𝐵 ∈ V) |
35 | | pwexg 5301 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → 𝒫 𝐵 ∈ V) |
36 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝐵𝑂𝒫 𝐵) = (𝐵𝑂𝒫 𝐵) |
37 | 5, 34, 35, 36 | fsovf1od 41624 |
. . . . . . . 8
⊢ (𝐵 ∈ V → (𝐵𝑂𝒫 𝐵):(𝒫 𝒫 𝐵 ↑m 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝒫 𝐵)) |
38 | 33, 37 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐵𝑂𝒫 𝐵):(𝒫 𝒫 𝐵 ↑m 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝒫 𝐵)) |
39 | | f1orel 6719 |
. . . . . . 7
⊢ ((𝐵𝑂𝒫 𝐵):(𝒫 𝒫 𝐵 ↑m 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝒫 𝐵) → Rel (𝐵𝑂𝒫 𝐵)) |
40 | | relbrcnvg 6013 |
. . . . . . 7
⊢ (Rel
(𝐵𝑂𝒫 𝐵) → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁))) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ 𝑁(𝐵𝑂𝒫 𝐵)(𝐺‘𝑁))) |
42 | 5, 34, 35, 36, 29 | fsovcnvd 41622 |
. . . . . . . 8
⊢ (𝐵 ∈ V → ◡(𝐵𝑂𝒫 𝐵) = (𝒫 𝐵𝑂𝐵)) |
43 | 42 | breqd 5085 |
. . . . . . 7
⊢ (𝐵 ∈ V → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁)) |
44 | 33, 43 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → ((𝐺‘𝑁)◡(𝐵𝑂𝒫 𝐵)𝑁 ↔ (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁)) |
45 | 32, 41, 44 | 3bitr2d 307 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑁𝐺(𝐺‘𝑁) ↔ (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁)) |
46 | 30, 45 | mpbid 231 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐺‘𝑁)(𝒫 𝐵𝑂𝐵)𝑁) |
47 | 5, 29, 46, 25, 27 | ntrneiel 41691 |
. . 3
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑋 ∈ ((𝐺‘𝑁)‘𝑆) ↔ 𝑆 ∈ (𝑁‘𝑋))) |
48 | | simpr3 1195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐷‘(𝐺‘𝑁))𝐹𝑀) |
49 | | difssd 4067 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∖ 𝑆) ⊆ 𝐵) |
50 | 4, 49 | sselpwd 5250 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) |
51 | 50 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) |
52 | 5, 8, 48, 25, 51 | ntrneiel 41691 |
. . . 4
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑋 ∈ ((𝐷‘(𝐺‘𝑁))‘(𝐵 ∖ 𝑆)) ↔ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |
53 | 52 | notbid 318 |
. . 3
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (¬ 𝑋 ∈ ((𝐷‘(𝐺‘𝑁))‘(𝐵 ∖ 𝑆)) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |
54 | 28, 47, 53 | 3bitr3d 309 |
. 2
⊢ ((𝜑 ∧ (𝑁𝐺(𝐺‘𝑁) ∧ (𝐺‘𝑁)𝐷(𝐷‘(𝐺‘𝑁)) ∧ (𝐷‘(𝐺‘𝑁))𝐹𝑀)) → (𝑆 ∈ (𝑁‘𝑋) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |
55 | 22, 54 | mpdan 684 |
1
⊢ (𝜑 → (𝑆 ∈ (𝑁‘𝑋) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) |