Metamath Proof Explorer


Theorem iunconnlem

Description: Lemma for iunconn . (Contributed by Mario Carneiro, 11-Jun-2014)

Ref Expression
Hypotheses iunconn.2 φ J TopOn X
iunconn.3 φ k A B X
iunconn.4 φ k A P B
iunconn.5 φ k A J 𝑡 B Conn
iunconn.6 φ U J
iunconn.7 φ V J
iunconn.8 φ V k A B
iunconn.9 φ U V X k A B
iunconn.10 φ k A B U V
iunconn.11 k φ
Assertion iunconnlem φ ¬ P U

Proof

Step Hyp Ref Expression
1 iunconn.2 φ J TopOn X
2 iunconn.3 φ k A B X
3 iunconn.4 φ k A P B
4 iunconn.5 φ k A J 𝑡 B Conn
5 iunconn.6 φ U J
6 iunconn.7 φ V J
7 iunconn.8 φ V k A B
8 iunconn.9 φ U V X k A B
9 iunconn.10 φ k A B U V
10 iunconn.11 k φ
11 n0 V k A B x x V k A B
12 7 11 sylib φ x x V k A B
13 elin x V k A B x V x k A B
14 eliun x k A B k A x B
15 nfv k x V
16 10 15 nfan k φ x V
17 nfv k ¬ P U
18 4 adantr φ k A x V x B J 𝑡 B Conn
19 1 ad2antrr φ k A x V x B P U J TopOn X
20 2 adantr φ k A x V x B P U B X
21 5 ad2antrr φ k A x V x B P U U J
22 6 ad2antrr φ k A x V x B P U V J
23 simprr φ k A x V x B P U P U
24 3 adantr φ k A x V x B P U P B
25 inelcm P U P B U B
26 23 24 25 syl2anc φ k A x V x B P U U B
27 inelcm x V x B V B
28 27 ad2antrl φ k A x V x B P U V B
29 8 ad2antrr φ k A x V x B P U U V X k A B
30 ssiun2 k A B k A B
31 30 ad2antlr φ k A x V x B P U B k A B
32 31 sscond φ k A x V x B P U X k A B X B
33 29 32 sstrd φ k A x V x B P U U V X B
34 inss1 U V U
35 toponss J TopOn X U J U X
36 19 21 35 syl2anc φ k A x V x B P U U X
37 34 36 sstrid φ k A x V x B P U U V X
38 reldisj U V X U V B = U V X B
39 37 38 syl φ k A x V x B P U U V B = U V X B
40 33 39 mpbird φ k A x V x B P U U V B =
41 9 ad2antrr φ k A x V x B P U k A B U V
42 31 41 sstrd φ k A x V x B P U B U V
43 19 20 21 22 26 28 40 42 nconnsubb φ k A x V x B P U ¬ J 𝑡 B Conn
44 43 expr φ k A x V x B P U ¬ J 𝑡 B Conn
45 18 44 mt2d φ k A x V x B ¬ P U
46 45 an4s φ x V k A x B ¬ P U
47 46 exp32 φ x V k A x B ¬ P U
48 16 17 47 rexlimd φ x V k A x B ¬ P U
49 14 48 syl5bi φ x V x k A B ¬ P U
50 49 expimpd φ x V x k A B ¬ P U
51 13 50 syl5bi φ x V k A B ¬ P U
52 51 exlimdv φ x x V k A B ¬ P U
53 12 52 mpd φ ¬ P U