This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunconnlem

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

Ref Expression
Hypotheses iunconn.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
iunconn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
iunconn.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
iunconn.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
iunconn.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
iunconn.7 ⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
iunconn.8 ⊢ ( 𝜑 → ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
iunconn.9 ⊢ ( 𝜑 → ( 𝑈 ∩ 𝑉 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
iunconn.10 ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑈 ∪ 𝑉 ) )
iunconn.11 ⊢ Ⅎ 𝑘 𝜑
Assertion iunconnlem ( 𝜑 → ¬ 𝑃 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 iunconn.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 iunconn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
3 iunconn.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
4 iunconn.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
5 iunconn.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
6 iunconn.7 ⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
7 iunconn.8 ⊢ ( 𝜑 → ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
8 iunconn.9 ⊢ ( 𝜑 → ( 𝑈 ∩ 𝑉 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
9 iunconn.10 ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑈 ∪ 𝑉 ) )
10 iunconn.11 ⊢ Ⅎ 𝑘 𝜑
11 n0 ⊢ ( ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
12 7 11 sylib ⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
13 elin ⊢ ( 𝑥 ∈ ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
14 eliun ⊢ ( 𝑥 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃ 𝑘 ∈ 𝐴 𝑥 ∈ 𝐵 )
15 nfv ⊢ Ⅎ 𝑘 𝑥 ∈ 𝑉
16 10 15 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ 𝑉 )
17 nfv ⊢ Ⅎ 𝑘 ¬ 𝑃 ∈ 𝑈
18 4 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
19 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
20 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝐵 ⊆ 𝑋 )
21 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝑈 ∈ 𝐽 )
22 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝑉 ∈ 𝐽 )
23 simprr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝑃 ∈ 𝑈 )
24 3 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝑃 ∈ 𝐵 )
25 inelcm ⊢ ( ( 𝑃 ∈ 𝑈 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑈 ∩ 𝐵 ) ≠ ∅ )
26 23 24 25 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( 𝑈 ∩ 𝐵 ) ≠ ∅ )
27 inelcm ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑉 ∩ 𝐵 ) ≠ ∅ )
28 27 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( 𝑉 ∩ 𝐵 ) ≠ ∅ )
29 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( 𝑈 ∩ 𝑉 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
30 ssiun2 ⊢ ( 𝑘 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑘 ∈ 𝐴 𝐵 )
31 30 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝐵 ⊆ ∪ 𝑘 ∈ 𝐴 𝐵 )
32 31 sscond ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ⊆ ( 𝑋 ∖ 𝐵 ) )
33 29 32 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( 𝑈 ∩ 𝑉 ) ⊆ ( 𝑋 ∖ 𝐵 ) )
34 inss1 ⊢ ( 𝑈 ∩ 𝑉 ) ⊆ 𝑈
35 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ 𝑋 )
36 19 21 35 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝑈 ⊆ 𝑋 )
37 34 36 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( 𝑈 ∩ 𝑉 ) ⊆ 𝑋 )
38 reldisj ⊢ ( ( 𝑈 ∩ 𝑉 ) ⊆ 𝑋 → ( ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐵 ) = ∅ ↔ ( 𝑈 ∩ 𝑉 ) ⊆ ( 𝑋 ∖ 𝐵 ) ) )
39 37 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐵 ) = ∅ ↔ ( 𝑈 ∩ 𝑉 ) ⊆ ( 𝑋 ∖ 𝐵 ) ) )
40 33 39 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐵 ) = ∅ )
41 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑈 ∪ 𝑉 ) )
42 31 41 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → 𝐵 ⊆ ( 𝑈 ∪ 𝑉 ) )
43 19 20 21 22 26 28 40 42 nconnsubb ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑈 ) ) → ¬ ( 𝐽 ↾t 𝐵 ) ∈ Conn )
44 43 expr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑃 ∈ 𝑈 → ¬ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) )
45 18 44 mt2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ) → ¬ 𝑃 ∈ 𝑈 )
46 45 an4s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ¬ 𝑃 ∈ 𝑈 )
47 46 exp32 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑘 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 → ¬ 𝑃 ∈ 𝑈 ) ) )
48 16 17 47 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ∃ 𝑘 ∈ 𝐴 𝑥 ∈ 𝐵 → ¬ 𝑃 ∈ 𝑈 ) )
49 14 48 biimtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 → ¬ 𝑃 ∈ 𝑈 ) )
50 49 expimpd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ¬ 𝑃 ∈ 𝑈 ) )
51 13 50 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ¬ 𝑃 ∈ 𝑈 ) )
52 51 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 ∈ ( 𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ¬ 𝑃 ∈ 𝑈 ) )
53 12 52 mpd ⊢ ( 𝜑 → ¬ 𝑃 ∈ 𝑈 )