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 44089 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
| 6 | | elmapi 8889 |
. . . . 5
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
| 8 | | ntrneiel2.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) |
| 9 | 7, 8 | ffvelcdmd 7105 |
. . 3
⊢ (𝜑 → (𝐼‘𝑆) ∈ 𝒫 𝐵) |
| 10 | 1, 2, 3, 4, 9 | ntrneiel 44094 |
. 2
⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐼‘𝑆)) ↔ (𝐼‘𝑆) ∈ (𝑁‘𝑋))) |
| 11 | 1, 2, 3, 8 | ntrneifv4 44098 |
. . . 4
⊢ (𝜑 → (𝐼‘𝑆) = {𝑦 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑦)}) |
| 12 | | df-rab 3437 |
. . . 4
⊢ {𝑦 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑦)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} |
| 13 | 11, 12 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → (𝐼‘𝑆) = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))}) |
| 14 | 13 | eleq1d 2826 |
. 2
⊢ (𝜑 → ((𝐼‘𝑆) ∈ (𝑁‘𝑋) ↔ {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋))) |
| 15 | | clabel 2888 |
. . . 4
⊢ ({𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋) ↔ ∃𝑢(𝑢 ∈ (𝑁‘𝑋) ∧ ∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
| 16 | | df-rex 3071 |
. . . 4
⊢
(∃𝑢 ∈
(𝑁‘𝑋)∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∃𝑢(𝑢 ∈ (𝑁‘𝑋) ∧ ∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
| 17 | 15, 16 | bitr4i 278 |
. . 3
⊢ ({𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
| 18 | | ibar 528 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝑆 ∈ (𝑁‘𝑦) ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
| 19 | 18 | bibi2d 342 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ((𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)) ↔ (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
| 20 | 19 | ralbiia 3091 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
| 21 | | ssv 4008 |
. . . . . . . 8
⊢ 𝐵 ⊆ V |
| 22 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → 𝐵 ⊆ V) |
| 23 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 24 | | eldif 3961 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (V ∖ 𝐵) ↔ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝐵)) |
| 25 | 23, 24 | mpbiran 709 |
. . . . . . . . 9
⊢ (𝑦 ∈ (V ∖ 𝐵) ↔ ¬ 𝑦 ∈ 𝐵) |
| 26 | 1, 2, 3 | ntrneinex 44090 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)) |
| 27 | | elmapi 8889 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (𝒫 𝒫
𝐵 ↑m 𝐵) → 𝑁:𝐵⟶𝒫 𝒫 𝐵) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁:𝐵⟶𝒫 𝒫 𝐵) |
| 29 | 28, 4 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁‘𝑋) ∈ 𝒫 𝒫 𝐵) |
| 30 | 29 | elpwid 4609 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘𝑋) ⊆ 𝒫 𝐵) |
| 31 | 30 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → 𝑢 ∈ 𝒫 𝐵) |
| 32 | 31 | elpwid 4609 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → 𝑢 ⊆ 𝐵) |
| 33 | 32 | sseld 3982 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (𝑦 ∈ 𝑢 → 𝑦 ∈ 𝐵)) |
| 34 | 33 | con3dimp 408 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) ∧ ¬ 𝑦 ∈ 𝐵) → ¬ 𝑦 ∈ 𝑢) |
| 35 | | pm3.14 998 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑦 ∈ 𝐵 ∨ ¬ 𝑆 ∈ (𝑁‘𝑦)) → ¬ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) |
| 36 | 35 | orcs 876 |
. . . . . . . . . . . 12
⊢ (¬
𝑦 ∈ 𝐵 → ¬ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) ∧ ¬ 𝑦 ∈ 𝐵) → ¬ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) |
| 38 | 34, 37 | 2falsed 376 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) ∧ ¬ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
| 39 | 38 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (¬ 𝑦 ∈ 𝐵 → (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
| 40 | 25, 39 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (𝑦 ∈ (V ∖ 𝐵) → (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
| 41 | 40 | ralrimiv 3145 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → ∀𝑦 ∈ (V ∖ 𝐵)(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
| 42 | 22, 41 | raldifeq 4494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∀𝑦 ∈ V (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
| 43 | 20, 42 | bitrid 283 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)) ↔ ∀𝑦 ∈ V (𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))))) |
| 44 | | ralv 3508 |
. . . . 5
⊢
(∀𝑦 ∈ V
(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦)))) |
| 45 | 43, 44 | bitr2di 288 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁‘𝑋)) → (∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |
| 46 | 45 | rexbidva 3177 |
. . 3
⊢ (𝜑 → (∃𝑢 ∈ (𝑁‘𝑋)∀𝑦(𝑦 ∈ 𝑢 ↔ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |
| 47 | 17, 46 | bitrid 283 |
. 2
⊢ (𝜑 → ({𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑆 ∈ (𝑁‘𝑦))} ∈ (𝑁‘𝑋) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |
| 48 | 10, 14, 47 | 3bitrd 305 |
1
⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐼‘𝑆)) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦)))) |