Users' Mathboxes Mathbox for Rohan Ridenour < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismnushort Structured version   Visualization version   GIF version

Theorem ismnushort 41900
Description: Express the predicate on 𝑈 and 𝑧 in ismnu 41860 in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024.)
Assertion
Ref Expression
ismnushort (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
Distinct variable groups:   𝑣,𝑈   𝑓,𝑖,𝑤,𝑧   𝑣,𝑓,𝑖,𝑧   𝑈,𝑓,𝑖,𝑢,𝑤
Allowed substitution hint:   𝑈(𝑧)

Proof of Theorem ismnushort
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 simpl 483 . . . . . 6 ((𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ (𝑈𝑤))
21reximi 3176 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤))
32ralimi 3087 . . . 4 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤))
4 0elpw 5276 . . . . . . . 8 ∅ ∈ 𝒫 𝑈
54a1i 11 . . . . . . 7 (⊤ → ∅ ∈ 𝒫 𝑈)
6 biidd 261 . . . . . . 7 ((⊤ ∧ 𝑓 = ∅) → (∃𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤) ↔ ∃𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤)))
75, 6rspcdv 3550 . . . . . 6 (⊤ → (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤) → ∃𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤)))
87mptru 1546 . . . . 5 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤) → ∃𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤))
9 inss1 4162 . . . . . . 7 (𝑈𝑤) ⊆ 𝑈
10 sstr2 3927 . . . . . . 7 (𝒫 𝑧 ⊆ (𝑈𝑤) → ((𝑈𝑤) ⊆ 𝑈 → 𝒫 𝑧𝑈))
119, 10mpi 20 . . . . . 6 (𝒫 𝑧 ⊆ (𝑈𝑤) → 𝒫 𝑧𝑈)
1211reximi 3176 . . . . 5 (∃𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤) → ∃𝑤𝑈 𝒫 𝑧𝑈)
138, 12syl 17 . . . 4 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 𝒫 𝑧 ⊆ (𝑈𝑤) → ∃𝑤𝑈 𝒫 𝑧𝑈)
14 rexex 3169 . . . . 5 (∃𝑤𝑈 𝒫 𝑧𝑈 → ∃𝑤𝒫 𝑧𝑈)
15 ax5e 1915 . . . . 5 (∃𝑤𝒫 𝑧𝑈 → 𝒫 𝑧𝑈)
1614, 15syl 17 . . . 4 (∃𝑤𝑈 𝒫 𝑧𝑈 → 𝒫 𝑧𝑈)
173, 13, 163syl 18 . . 3 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧𝑈)
18 inss1 4162 . . . . . . . 8 (𝑈𝑔) ⊆ 𝑈
19 vex 3433 . . . . . . . . . 10 𝑔 ∈ V
2019inex2 5240 . . . . . . . . 9 (𝑈𝑔) ∈ V
2120elpw 4537 . . . . . . . 8 ((𝑈𝑔) ∈ 𝒫 𝑈 ↔ (𝑈𝑔) ⊆ 𝑈)
2218, 21mpbir 230 . . . . . . 7 (𝑈𝑔) ∈ 𝒫 𝑈
23 unieq 4850 . . . . . . . . . . . 12 (𝑓 = (𝑈𝑔) → 𝑓 = (𝑈𝑔))
2423ineq2d 4146 . . . . . . . . . . 11 (𝑓 = (𝑈𝑔) → (𝑧 𝑓) = (𝑧 (𝑈𝑔)))
25 ineq1 4139 . . . . . . . . . . . 12 (𝑓 = (𝑈𝑔) → (𝑓 ∩ 𝒫 𝒫 𝑤) = ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤))
2625unieqd 4853 . . . . . . . . . . 11 (𝑓 = (𝑈𝑔) → (𝑓 ∩ 𝒫 𝒫 𝑤) = ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤))
2724, 26sseq12d 3953 . . . . . . . . . 10 (𝑓 = (𝑈𝑔) → ((𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)))
2827anbi2d 629 . . . . . . . . 9 (𝑓 = (𝑈𝑔) → ((𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤))))
2928rexbidv 3224 . . . . . . . 8 (𝑓 = (𝑈𝑔) → (∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤))))
3029rspcv 3554 . . . . . . 7 ((𝑈𝑔) ∈ 𝒫 𝑈 → (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤))))
3122, 30ax-mp 5 . . . . . 6 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)))
3231alrimiv 1930 . . . . 5 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)))
33 inss2 4163 . . . . . . . 8 (𝑈𝑤) ⊆ 𝑤
34 sstr2 3927 . . . . . . . 8 (𝒫 𝑧 ⊆ (𝑈𝑤) → ((𝑈𝑤) ⊆ 𝑤 → 𝒫 𝑧𝑤))
3533, 34mpi 20 . . . . . . 7 (𝒫 𝑧 ⊆ (𝑈𝑤) → 𝒫 𝑧𝑤)
36 an12 642 . . . . . . . . . . . 12 ((𝑣𝑈 ∧ (𝑖𝑣𝑣𝑔)) ↔ (𝑖𝑣 ∧ (𝑣𝑈𝑣𝑔)))
37 elin 3902 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝑈𝑔) ↔ (𝑣𝑈𝑣𝑔))
3837bicomi 223 . . . . . . . . . . . . 13 ((𝑣𝑈𝑣𝑔) ↔ 𝑣 ∈ (𝑈𝑔))
3938anbi2i 623 . . . . . . . . . . . 12 ((𝑖𝑣 ∧ (𝑣𝑈𝑣𝑔)) ↔ (𝑖𝑣𝑣 ∈ (𝑈𝑔)))
4036, 39bitri 274 . . . . . . . . . . 11 ((𝑣𝑈 ∧ (𝑖𝑣𝑣𝑔)) ↔ (𝑖𝑣𝑣 ∈ (𝑈𝑔)))
4140exbii 1850 . . . . . . . . . 10 (∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑔)) ↔ ∃𝑣(𝑖𝑣𝑣 ∈ (𝑈𝑔)))
42 df-rex 3070 . . . . . . . . . 10 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑔)))
43 eluni 4842 . . . . . . . . . 10 (𝑖 (𝑈𝑔) ↔ ∃𝑣(𝑖𝑣𝑣 ∈ (𝑈𝑔)))
4441, 42, 433bitr4i 303 . . . . . . . . 9 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) ↔ 𝑖 (𝑈𝑔))
45 simp1 1135 . . . . . . . . . . . . 13 (((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖𝑧𝑖 (𝑈𝑔)) → (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤))
46 elin 3902 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑧 (𝑈𝑔)) ↔ (𝑖𝑧𝑖 (𝑈𝑔)))
4746biimpri 227 . . . . . . . . . . . . . 14 ((𝑖𝑧𝑖 (𝑈𝑔)) → 𝑖 ∈ (𝑧 (𝑈𝑔)))
48473adant1 1129 . . . . . . . . . . . . 13 (((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖𝑧𝑖 (𝑈𝑔)) → 𝑖 ∈ (𝑧 (𝑈𝑔)))
4945, 48sseldd 3921 . . . . . . . . . . . 12 (((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖𝑧𝑖 (𝑈𝑔)) → 𝑖 ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤))
50 eluni 4842 . . . . . . . . . . . 12 (𝑖 ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖𝑢𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)))
5149, 50sylib 217 . . . . . . . . . . 11 (((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖𝑧𝑖 (𝑈𝑔)) → ∃𝑢(𝑖𝑢𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)))
52 elinel1 4128 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ (𝑈𝑔))
5352elin2d 4132 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢𝑔)
54 elinel2 4129 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝒫 𝒫 𝑤)
55 elpwpw 5030 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ (𝑢 ∈ V ∧ 𝑢𝑤))
5655simprbi 497 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ 𝒫 𝒫 𝑤 𝑢𝑤)
5754, 56syl 17 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢𝑤)
5853, 57jca 512 . . . . . . . . . . . . . . 15 (𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) → (𝑢𝑔 𝑢𝑤))
5958anim2i 617 . . . . . . . . . . . . . 14 ((𝑖𝑢𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑖𝑢 ∧ (𝑢𝑔 𝑢𝑤)))
60 an12 642 . . . . . . . . . . . . . 14 ((𝑖𝑢 ∧ (𝑢𝑔 𝑢𝑤)) ↔ (𝑢𝑔 ∧ (𝑖𝑢 𝑢𝑤)))
6159, 60sylib 217 . . . . . . . . . . . . 13 ((𝑖𝑢𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑢𝑔 ∧ (𝑖𝑢 𝑢𝑤)))
6261eximi 1837 . . . . . . . . . . . 12 (∃𝑢(𝑖𝑢𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢(𝑢𝑔 ∧ (𝑖𝑢 𝑢𝑤)))
63 df-rex 3070 . . . . . . . . . . . 12 (∃𝑢𝑔 (𝑖𝑢 𝑢𝑤) ↔ ∃𝑢(𝑢𝑔 ∧ (𝑖𝑢 𝑢𝑤)))
6462, 63sylibr 233 . . . . . . . . . . 11 (∃𝑢(𝑖𝑢𝑢 ∈ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))
6551, 64syl 17 . . . . . . . . . 10 (((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖𝑧𝑖 (𝑈𝑔)) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))
66653expia 1120 . . . . . . . . 9 (((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖𝑧) → (𝑖 (𝑈𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤)))
6744, 66syl5bi 241 . . . . . . . 8 (((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖𝑧) → (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤)))
6867ralrimiva 3108 . . . . . . 7 ((𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤) → ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤)))
6935, 68anim12i 613 . . . . . 6 ((𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))))
7069reximi 3176 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 (𝑈𝑔)) ⊆ ((𝑈𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))))
7132, 70sylg 1825 . . . 4 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))))
72 elequ2 2121 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑣𝑓𝑣𝑔))
7372anbi2d 629 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑖𝑣𝑣𝑓) ↔ (𝑖𝑣𝑣𝑔)))
7473rexbidv 3224 . . . . . . . . 9 (𝑓 = 𝑔 → (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑔)))
75 rexeq 3341 . . . . . . . . 9 (𝑓 = 𝑔 → (∃𝑢𝑓 (𝑖𝑢 𝑢𝑤) ↔ ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤)))
7674, 75imbi12d 345 . . . . . . . 8 (𝑓 = 𝑔 → ((∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))))
7776ralbidv 3121 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))))
7877anbi2d 629 . . . . . 6 (𝑓 = 𝑔 → ((𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤)))))
7978rexbidv 3224 . . . . 5 (𝑓 = 𝑔 → (∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤)))))
8079cbvalvw 2039 . . . 4 (∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ∀𝑔𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑔) → ∃𝑢𝑔 (𝑖𝑢 𝑢𝑤))))
8171, 80sylibr 233 . . 3 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
8217, 81jca 512 . 2 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
83 nfv 1917 . . . 4 𝑓𝒫 𝑧𝑈
84 nfa1 2148 . . . 4 𝑓𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
8583, 84nfan 1902 . . 3 𝑓(𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
86 elpwi 4542 . . . 4 (𝑓 ∈ 𝒫 𝑈𝑓𝑈)
87 sp 2176 . . . . . 6 (∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) → ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
88 ssin 4164 . . . . . . . . . . . . 13 ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ↔ 𝒫 𝑧 ⊆ (𝑈𝑤))
8988biimpi 215 . . . . . . . . . . . 12 ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) → 𝒫 𝑧 ⊆ (𝑈𝑤))
9089ex 413 . . . . . . . . . . 11 (𝒫 𝑧𝑈 → (𝒫 𝑧𝑤 → 𝒫 𝑧 ⊆ (𝑈𝑤)))
9190adantr 481 . . . . . . . . . 10 ((𝒫 𝑧𝑈𝑓𝑈) → (𝒫 𝑧𝑤 → 𝒫 𝑧 ⊆ (𝑈𝑤)))
92 simp3 1137 . . . . . . . . . . . . . . . . 17 ((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) → 𝑖 𝑓)
93 eluni 4842 . . . . . . . . . . . . . . . . 17 (𝑖 𝑓 ↔ ∃𝑣(𝑖𝑣𝑣𝑓))
9492, 93sylib 217 . . . . . . . . . . . . . . . 16 ((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) → ∃𝑣(𝑖𝑣𝑣𝑓))
95 simpl2 1191 . . . . . . . . . . . . . . . . . . . 20 (((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) ∧ (𝑖𝑣𝑣𝑓)) → 𝑓𝑈)
96 simprr 770 . . . . . . . . . . . . . . . . . . . 20 (((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) ∧ (𝑖𝑣𝑣𝑓)) → 𝑣𝑓)
9795, 96sseldd 3921 . . . . . . . . . . . . . . . . . . 19 (((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) ∧ (𝑖𝑣𝑣𝑓)) → 𝑣𝑈)
98 simprl 768 . . . . . . . . . . . . . . . . . . 19 (((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) ∧ (𝑖𝑣𝑣𝑓)) → 𝑖𝑣)
9997, 98, 963jca 1127 . . . . . . . . . . . . . . . . . 18 (((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) ∧ (𝑖𝑣𝑣𝑓)) → (𝑣𝑈𝑖𝑣𝑣𝑓))
10099ex 413 . . . . . . . . . . . . . . . . 17 ((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) → ((𝑖𝑣𝑣𝑓) → (𝑣𝑈𝑖𝑣𝑣𝑓)))
101100eximdv 1920 . . . . . . . . . . . . . . . 16 ((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) → (∃𝑣(𝑖𝑣𝑣𝑓) → ∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓)))
10294, 101mpd 15 . . . . . . . . . . . . . . 15 ((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) → ∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓))
103 df-rex 3070 . . . . . . . . . . . . . . . 16 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
104 3anass 1094 . . . . . . . . . . . . . . . . 17 ((𝑣𝑈𝑖𝑣𝑣𝑓) ↔ (𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
105104exbii 1850 . . . . . . . . . . . . . . . 16 (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
106103, 105bitr4i 277 . . . . . . . . . . . . . . 15 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓))
107102, 106sylibr 233 . . . . . . . . . . . . . 14 ((𝒫 𝑧𝑈𝑓𝑈𝑖 𝑓) → ∃𝑣𝑈 (𝑖𝑣𝑣𝑓))
1081073expia 1120 . . . . . . . . . . . . 13 ((𝒫 𝑧𝑈𝑓𝑈) → (𝑖 𝑓 → ∃𝑣𝑈 (𝑖𝑣𝑣𝑓)))
109 elin 3902 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢𝑓𝑢 ∈ 𝒫 𝒫 𝑤))
110 vex 3433 . . . . . . . . . . . . . . . . . . . . . 22 𝑢 ∈ V
111110, 55mpbiran 706 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ 𝒫 𝒫 𝑤 𝑢𝑤)
112111anbi2i 623 . . . . . . . . . . . . . . . . . . . 20 ((𝑢𝑓𝑢 ∈ 𝒫 𝒫 𝑤) ↔ (𝑢𝑓 𝑢𝑤))
113109, 112bitri 274 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢𝑓 𝑢𝑤))
114113anbi2i 623 . . . . . . . . . . . . . . . . . 18 ((𝑖𝑢𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖𝑢 ∧ (𝑢𝑓 𝑢𝑤)))
115 an12 642 . . . . . . . . . . . . . . . . . 18 ((𝑢𝑓 ∧ (𝑖𝑢 𝑢𝑤)) ↔ (𝑖𝑢 ∧ (𝑢𝑓 𝑢𝑤)))
116114, 115bitr4i 277 . . . . . . . . . . . . . . . . 17 ((𝑖𝑢𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑢𝑓 ∧ (𝑖𝑢 𝑢𝑤)))
117116exbii 1850 . . . . . . . . . . . . . . . 16 (∃𝑢(𝑖𝑢𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑢(𝑢𝑓 ∧ (𝑖𝑢 𝑢𝑤)))
118 eluni 4842 . . . . . . . . . . . . . . . 16 (𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖𝑢𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)))
119 df-rex 3070 . . . . . . . . . . . . . . . 16 (∃𝑢𝑓 (𝑖𝑢 𝑢𝑤) ↔ ∃𝑢(𝑢𝑓 ∧ (𝑖𝑢 𝑢𝑤)))
120117, 118, 1193bitr4i 303 . . . . . . . . . . . . . . 15 (𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))
121120biimpri 227 . . . . . . . . . . . . . 14 (∃𝑢𝑓 (𝑖𝑢 𝑢𝑤) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤))
122121a1i 11 . . . . . . . . . . . . 13 ((𝒫 𝑧𝑈𝑓𝑈) → (∃𝑢𝑓 (𝑖𝑢 𝑢𝑤) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)))
123108, 122imim12d 81 . . . . . . . . . . . 12 ((𝒫 𝑧𝑈𝑓𝑈) → ((∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) → (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤))))
124123ralimdv 3104 . . . . . . . . . . 11 ((𝒫 𝑧𝑈𝑓𝑈) → (∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) → ∀𝑖𝑧 (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤))))
125 elin 3902 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑧 𝑓) ↔ (𝑖𝑧𝑖 𝑓))
126125imbi1i 350 . . . . . . . . . . . . . 14 ((𝑖 ∈ (𝑧 𝑓) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ((𝑖𝑧𝑖 𝑓) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)))
127 impexp 451 . . . . . . . . . . . . . 14 (((𝑖𝑧𝑖 𝑓) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖𝑧 → (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤))))
128126, 127bitri 274 . . . . . . . . . . . . 13 ((𝑖 ∈ (𝑧 𝑓) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖𝑧 → (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤))))
129128albii 1822 . . . . . . . . . . . 12 (∀𝑖(𝑖 ∈ (𝑧 𝑓) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖𝑧 → (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤))))
130 dfss2 3906 . . . . . . . . . . . 12 ((𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖(𝑖 ∈ (𝑧 𝑓) → 𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)))
131 df-ral 3069 . . . . . . . . . . . 12 (∀𝑖𝑧 (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖𝑧 → (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤))))
132129, 130, 1313bitr4i 303 . . . . . . . . . . 11 ((𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖𝑧 (𝑖 𝑓𝑖 (𝑓 ∩ 𝒫 𝒫 𝑤)))
133124, 132syl6ibr 251 . . . . . . . . . 10 ((𝒫 𝑧𝑈𝑓𝑈) → (∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) → (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)))
13491, 133anim12d 609 . . . . . . . . 9 ((𝒫 𝑧𝑈𝑓𝑈) → ((𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) → (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤))))
135134reximdv 3200 . . . . . . . 8 ((𝒫 𝑧𝑈𝑓𝑈) → (∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤))))
1361353impia 1116 . . . . . . 7 ((𝒫 𝑧𝑈𝑓𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)))
1371363com23 1125 . . . . . 6 ((𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ∧ 𝑓𝑈) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)))
13887, 137syl3an2 1163 . . . . 5 ((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ∧ 𝑓𝑈) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)))
1391383expa 1117 . . . 4 (((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ∧ 𝑓𝑈) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)))
14086, 139sylan2 593 . . 3 (((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ∧ 𝑓 ∈ 𝒫 𝑈) → ∃𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)))
14185, 140ralrimia 3427 . 2 ((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) → ∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)))
14282, 141impbii 208 1 (∀𝑓 ∈ 𝒫 𝑈𝑤𝑈 (𝒫 𝑧 ⊆ (𝑈𝑤) ∧ (𝑧 𝑓) ⊆ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086  wal 1537   = wceq 1539  wtru 1540  wex 1782  wcel 2106  wral 3064  wrex 3065  Vcvv 3429  cin 3885  wss 3886  c0 4256  𝒫 cpw 4533   cuni 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3431  df-dif 3889  df-in 3893  df-ss 3903  df-nul 4257  df-pw 4535  df-uni 4840
This theorem is referenced by:  dfuniv2  41901
  Copyright terms: Public domain W3C validator