Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neiptopuni Structured version   Unicode version

Theorem neiptopuni 19758
 Description: Lemma for neiptopreu 19761 (Contributed by Thierry Arnoux, 6-Jan-2018.)
Hypotheses
Ref Expression
neiptop.o
neiptop.0
neiptop.1
neiptop.2
neiptop.3
neiptop.4
neiptop.5
Assertion
Ref Expression
neiptopuni
Distinct variable groups:   ,   ,   ,   ,,   ,,   ,   ,
Allowed substitution hints:   (,,)   (,)   (,,)   (,)

Proof of Theorem neiptopuni
StepHypRef Expression
1 elpwi 4024 . . . . . . . 8
21ad2antlr 726 . . . . . . 7
3 simpr 461 . . . . . . 7
42, 3sseldd 3500 . . . . . 6
5 neiptop.o . . . . . . . . . 10
65unieqi 4260 . . . . . . . . 9
76eleq2i 2535 . . . . . . . 8
8 elunirab 4263 . . . . . . . 8
97, 8bitri 249 . . . . . . 7
10 simpl 457 . . . . . . . 8
1110reximi 2925 . . . . . . 7
129, 11sylbi 195 . . . . . 6
134, 12r19.29a 2999 . . . . 5
1413a1i 11 . . . 4
1514ssrdv 3505 . . 3
16 ssid 3518 . . . . 5
1716a1i 11 . . . 4
18 neiptop.5 . . . . 5
1918ralrimiva 2871 . . . 4
205neipeltop 19757 . . . 4
2117, 19, 20sylanbrc 664 . . 3
22 unissel 4282 . . 3
2315, 21, 22syl2anc 661 . 2
2423eqcomd 2465 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 973   wceq 1395   wcel 1819  wral 2807  wrex 2808  crab 2811   wss 3471  cpw 4015  cuni 4251  wf 5590  cfv 5594  cfi 7888 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-nul 4586 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3794  df-pw 4017  df-uni 4252 This theorem is referenced by:  neiptoptop  19759  neiptopnei  19760  neiptopreu  19761
 Copyright terms: Public domain W3C validator