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 ( 𝜑 → ( 𝐴𝑈𝐵𝑈 ) )