Proof of Theorem ntrneiel2
Step | Hyp | Ref
| Expression |
1 | | ntrnei.o |
. . 3
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) |
2 | | ntrnei.f |
. . 3
⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) |
3 | | ntrnei.r |
. . 3
⊢ (𝜑 → 𝐼𝐹𝑁) |
4 | | ntrneiel2.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
5 | 1, 2, 3 | ntrneiiex 41686 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
6 | | elmapi 8637 |
. . . . 5
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
8 | | ntrneiel2.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) |
9 | 7, 8 | ffvelrnd 6962 |
. . 3
⊢ (𝜑 → (𝐼‘𝑆) ∈ 𝒫 𝐵) |
10 | 1, 2, 3, 4, 9 | ntrneiel 41691 |
. 2
⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐼‘𝑆)) ↔ (𝐼‘𝑆) ∈ (𝑁‘𝑋))) |
11 | 1, 2, 3, 8 | ntrneifv4 41695 |
. . . 4
⊢ (𝜑 → (𝐼‘𝑆) = {𝑦 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑦)}) |
12 | | df-rab 3073 |
. . . 4
⊢ {𝑦 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑦)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} |
13 | 11, 12 | eqtrdi 2794 |
. . 3
⊢ (𝜑 → (𝐼‘𝑆) = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))}) |
14 | 13 | eleq1d 2823 |
. 2
⊢ (𝜑 → ((𝐼‘𝑆) ∈ (𝑁‘𝑋) ↔ {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋))) |
15 | | clabel 2885 |
. . . 4
⊢ ({𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋) ↔ ∃𝑢(𝑢 ∈ (𝑁‘𝑋) ∧ ∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
16 | | df-rex 3070 |
. . . 4
⊢
(∃𝑢 ∈
(𝑁‘𝑋)∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∃𝑢(𝑢 ∈ (𝑁‘𝑋) ∧ ∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
17 | 15, 16 | bitr4i 277 |
. . 3
⊢ ({𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
18 | | ibar 529 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝑆 ∈ (𝑁‘𝑦) ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
19 | 18 | bibi2d 343 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ((𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)) ↔ (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
20 | 19 | ralbiia 3091 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
21 | | ssv 3945 |
. . . . . . . 8
⊢ 𝐵 ⊆ V |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → 𝐵 ⊆ V) |
23 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
24 | | eldif 3897 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (V ∖ 𝐵) ↔ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝐵)) |
25 | 23, 24 | mpbiran 706 |
. . . . . . . . 9
⊢ (𝑦 ∈ (V ∖ 𝐵) ↔ ¬ 𝑦 ∈ 𝐵) |
26 | 1, 2, 3 | ntrneinex 41687 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)) |
27 | | elmapi 8637 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (𝒫 𝒫
𝐵 ↑m 𝐵) → 𝑁:𝐵⟶𝒫 𝒫 𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁:𝐵⟶𝒫 𝒫 𝐵) |
29 | 28, 4 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁‘𝑋) ∈ 𝒫 𝒫 𝐵) |
30 | 29 | elpwid 4544 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘𝑋) ⊆ 𝒫 𝐵) |
31 | 30 | sselda 3921 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → 𝑢 ∈ 𝒫 𝐵) |
32 | 31 | elpwid 4544 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → 𝑢 ⊆ 𝐵) |
33 | 32 | sseld 3920 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (𝑦 ∈ 𝑢 → 𝑦 ∈ 𝐵)) |
34 | 33 | con3dimp 409 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) ∧ ¬ 𝑦 ∈ 𝐵) → ¬ 𝑦 ∈ 𝑢) |
35 | | pm3.14 993 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑦 ∈ 𝐵 ∨ ¬ 𝑆 ∈ (𝑁‘𝑦)) → ¬ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) |
36 | 35 | orcs 872 |
. . . . . . . . . . . 12
⊢ (¬
𝑦 ∈ 𝐵 → ¬ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) |
37 | 36 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) ∧ ¬ 𝑦 ∈ 𝐵) → ¬ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) |
38 | 34, 37 | 2falsed 377 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) ∧ ¬ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
39 | 38 | ex 413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (¬ 𝑦 ∈ 𝐵 → (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
40 | 25, 39 | syl5bi 241 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (𝑦 ∈ (V ∖ 𝐵) → (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
41 | 40 | ralrimiv 3102 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → ∀𝑦 ∈ (V ∖ 𝐵)(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
42 | 22, 41 | raldifeq 4424 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∀𝑦 ∈ V (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
43 | 20, 42 | bitrid 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)) ↔ ∀𝑦 ∈ V (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
44 | | ralv 3456 |
. . . . 5
⊢
(∀𝑦 ∈ V
(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
45 | 43, 44 | bitr2di 288 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |
46 | 45 | rexbidva 3225 |
. . 3
⊢ (𝜑 → (∃𝑢 ∈ (𝑁‘𝑋)∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |
47 | 17, 46 | bitrid 282 |
. 2
⊢ (𝜑 → ({𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |
48 | 10, 14, 47 | 3bitrd 305 |
1
⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐼‘𝑆)) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |