Proof of Theorem ntrneik13
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfss3 3972 | . . . . . . . . 9
⊢ ((𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))) | 
| 2 |  | ntrnei.o | . . . . . . . . . . . . . . 15
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) | 
| 3 |  | ntrnei.f | . . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) | 
| 4 |  | ntrnei.r | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼𝐹𝑁) | 
| 5 | 2, 3, 4 | ntrneiiex 44089 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) | 
| 6 |  | elmapi 8889 | . . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) | 
| 7 | 5, 6 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵) | 
| 8 | 7 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) | 
| 9 | 2, 3, 4 | ntrneibex 44086 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ V) | 
| 10 | 9 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝐵 ∈ V) | 
| 11 |  | simplr 769 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵) | 
| 12 |  | elpwi 4607 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵) | 
| 13 |  | ssinss1 4246 | . . . . . . . . . . . . . 14
⊢ (𝑠 ⊆ 𝐵 → (𝑠 ∩ 𝑡) ⊆ 𝐵) | 
| 14 | 11, 12, 13 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑠 ∩ 𝑡) ⊆ 𝐵) | 
| 15 | 10, 14 | sselpwd 5328 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑠 ∩ 𝑡) ∈ 𝒫 𝐵) | 
| 16 | 8, 15 | ffvelcdmd 7105 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝑠 ∩ 𝑡)) ∈ 𝒫 𝐵) | 
| 17 | 16 | elpwid 4609 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘(𝑠 ∩ 𝑡)) ⊆ 𝐵) | 
| 18 |  | ralss 4058 | . . . . . . . . . 10
⊢ ((𝐼‘(𝑠 ∩ 𝑡)) ⊆ 𝐵 → (∀𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) → 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))))) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) → 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))))) | 
| 20 | 1, 19 | bitrid 283 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) → 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))))) | 
| 21 |  | dfss3 3972 | . . . . . . . . 9
⊢ (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))) | 
| 22 | 7 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐼‘𝑠) ∈ 𝒫 𝐵) | 
| 23 | 22 | elpwid 4609 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐼‘𝑠) ⊆ 𝐵) | 
| 24 |  | ssinss1 4246 | . . . . . . . . . . . 12
⊢ ((𝐼‘𝑠) ⊆ 𝐵 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ 𝐵) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ 𝐵) | 
| 26 | 25 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ 𝐵) | 
| 27 |  | ralss 4058 | . . . . . . . . . 10
⊢ (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ 𝐵 → (∀𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))))) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))))) | 
| 29 | 21, 28 | bitrid 283 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))))) | 
| 30 | 20, 29 | anbi12d 632 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ∧ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡))) ↔ (∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) → 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))) ∧ ∀𝑥 ∈ 𝐵 (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)))))) | 
| 31 |  | eqss 3999 | . . . . . . 7
⊢ ((𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ((𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ∧ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)))) | 
| 32 |  | ralbiim 3113 | . . . . . . 7
⊢
(∀𝑥 ∈
𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) ↔ 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))) ↔ (∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) → 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))) ∧ ∀𝑥 ∈ 𝐵 (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡))))) | 
| 33 | 30, 31, 32 | 3bitr4g 314 | . . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) ↔ 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))))) | 
| 34 | 4 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝐼𝐹𝑁) | 
| 35 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) | 
| 36 | 9 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐵 ∈ V) | 
| 37 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵) | 
| 38 | 37 | elpwid 4609 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ⊆ 𝐵) | 
| 39 | 38, 13 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝑠 ∩ 𝑡) ⊆ 𝐵) | 
| 40 | 36, 39 | sselpwd 5328 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝑠 ∩ 𝑡) ∈ 𝒫 𝐵) | 
| 41 | 40 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑠 ∩ 𝑡) ∈ 𝒫 𝐵) | 
| 42 | 2, 3, 34, 35, 41 | ntrneiel 44094 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) ↔ (𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥))) | 
| 43 |  | elin 3967 | . . . . . . . . 9
⊢ (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡))) | 
| 44 |  | simpllr 776 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑠 ∈ 𝒫 𝐵) | 
| 45 | 2, 3, 34, 35, 44 | ntrneiel 44094 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝐼‘𝑠) ↔ 𝑠 ∈ (𝑁‘𝑥))) | 
| 46 |  | simplr 769 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑡 ∈ 𝒫 𝐵) | 
| 47 | 2, 3, 34, 35, 46 | ntrneiel 44094 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝐼‘𝑡) ↔ 𝑡 ∈ (𝑁‘𝑥))) | 
| 48 | 45, 47 | anbi12d 632 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))) | 
| 49 | 43, 48 | bitrid 283 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))) | 
| 50 | 42, 49 | bibi12d 345 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) ↔ 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))) ↔ ((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))))) | 
| 51 | 50 | ralbidva 3176 | . . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝐼‘(𝑠 ∩ 𝑡)) ↔ 𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))) ↔ ∀𝑥 ∈ 𝐵 ((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))))) | 
| 52 | 33, 51 | bitrd 279 | . . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))))) | 
| 53 | 52 | ralbidva 3176 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝐵∀𝑥 ∈ 𝐵 ((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))))) | 
| 54 |  | ralcom 3289 | . . . 4
⊢
(∀𝑡 ∈
𝒫 𝐵∀𝑥 ∈ 𝐵 ((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))) | 
| 55 | 53, 54 | bitrdi 287 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))))) | 
| 56 | 55 | ralbidva 3176 | . 2
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑥 ∈ 𝐵 ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))))) | 
| 57 |  | ralcom 3289 | . 2
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑥 ∈ 𝐵 ∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))) | 
| 58 | 56, 57 | bitrdi 287 | 1
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥))))) |