Metamath Proof Explorer

Theorem regr1lem

Description: Lemma for regr1 . (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
regr1lem.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
regr1lem.3 ⊢ ( 𝜑 → 𝐽 ∈ Reg )
regr1lem.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
regr1lem.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
regr1lem.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
regr1lem.7 ⊢ ( 𝜑 → ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
Assertion regr1lem ( 𝜑 → ( 𝐴 ∈ 𝑈 → 𝐵 ∈ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 regr1lem.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 regr1lem.3 ⊢ ( 𝜑 → 𝐽 ∈ Reg )
4 regr1lem.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
5 regr1lem.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
6 regr1lem.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
7 regr1lem.7 ⊢ ( 𝜑 → ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
8 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 𝐽 ∈ Reg )
9 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 𝑈 ∈ 𝐽 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ∈ 𝑈 )
11 regsep ⊢ ( ( 𝐽 ∈ Reg ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) )
12 8 9 10 11 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) )
13 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) → ¬ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
14 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝑧 ∈ 𝐽 )
16 1 kqopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) )
17 14 15 16 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) )
18 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
19 14 18 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝑋 = ∪ 𝐽 )
20 19 difeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) = ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) )
21 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
22 14 21 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝐽 ∈ Top )
23 elssuni ⊢ ( 𝑧 ∈ 𝐽 → 𝑧 ⊆ ∪ 𝐽 )
24 15 23 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝑧 ⊆ ∪ 𝐽 )
25 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
26 25 clscld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ∈ ( Clsd ‘ 𝐽 ) )
27 22 24 26 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ∈ ( Clsd ‘ 𝐽 ) )
28 25 cldopn ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ∈ 𝐽 )
29 27 28 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ∈ 𝐽 )
30 20 29 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ∈ 𝐽 )
31 1 kqopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ∈ 𝐽 ) → ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ∈ ( KQ ‘ 𝐽 ) )
32 14 30 31 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ∈ ( KQ ‘ 𝐽 ) )
33 simprrl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) → 𝐴 ∈ 𝑧 )
34 33 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝐴 ∈ 𝑧 )
35 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝐴 ∈ 𝑋 )
36 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑧 ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) ) )
37 14 15 35 36 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝐴 ∈ 𝑧 ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) ) )
38 34 37 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) )
39 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝐵 ∈ 𝑋 )
40 simprrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 )
41 40 sseld ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) → ( 𝐵 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) → 𝐵 ∈ 𝑈 ) )
42 41 con3dimp ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ¬ 𝐵 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) )
43 39 42 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝐵 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) )
44 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ∈ 𝐽 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) )
45 14 30 39 44 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝐵 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) )
46 43 45 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) )
47 25 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ⊆ ∪ 𝐽 ) → 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) )
48 22 24 47 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) )
49 48 sscond ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) )
50 imass2 ⊢ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) → ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ⊆ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) )
51 sslin ⊢ ( ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ⊆ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) → ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) ⊆ ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) ) )
52 49 50 51 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) ⊆ ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) ) )
53 1 kqdisj ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) ) = ∅ )
54 14 15 53 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) ) = ∅ )
55 sseq0 ⊢ ( ( ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) ⊆ ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) ) ∧ ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ 𝑧 ) ) ) = ∅ ) → ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) = ∅ )
56 52 54 55 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) = ∅ )
57 eleq2 ⊢ ( 𝑚 = ( 𝐹 “ 𝑧 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) ) )
58 ineq1 ⊢ ( 𝑚 = ( 𝐹 “ 𝑧 ) → ( 𝑚 ∩ 𝑛 ) = ( ( 𝐹 “ 𝑧 ) ∩ 𝑛 ) )
59 58 eqeq1d ⊢ ( 𝑚 = ( 𝐹 “ 𝑧 ) → ( ( 𝑚 ∩ 𝑛 ) = ∅ ↔ ( ( 𝐹 “ 𝑧 ) ∩ 𝑛 ) = ∅ ) )
60 57 59 3anbi13d ⊢ ( 𝑚 = ( 𝐹 “ 𝑧 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( ( 𝐹 “ 𝑧 ) ∩ 𝑛 ) = ∅ ) ) )
61 eleq2 ⊢ ( 𝑛 = ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) → ( ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) )
62 ineq2 ⊢ ( 𝑛 = ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) → ( ( 𝐹 “ 𝑧 ) ∩ 𝑛 ) = ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) )
63 62 eqeq1d ⊢ ( 𝑛 = ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) → ( ( ( 𝐹 “ 𝑧 ) ∩ 𝑛 ) = ∅ ↔ ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) = ∅ ) )
64 61 63 3anbi23d ⊢ ( 𝑛 = ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( ( 𝐹 “ 𝑧 ) ∩ 𝑛 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ∧ ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) = ∅ ) ) )
65 60 64 rspc2ev ⊢ ( ( ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) ∧ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝑧 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ∧ ( ( 𝐹 “ 𝑧 ) ∩ ( 𝐹 “ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) ) ) = ∅ ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
66 17 32 38 46 56 65 syl113anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) ∧ ¬ 𝐵 ∈ 𝑈 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
67 66 ex ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) → ( ¬ 𝐵 ∈ 𝑈 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑚 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
68 13 67 mt3d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑧 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑈 ) ) ) → 𝐵 ∈ 𝑈 )
69 12 68 rexlimddv ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 𝐵 ∈ 𝑈 )
70 69 ex ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑈 → 𝐵 ∈ 𝑈 ) )