Metamath Proof Explorer

Theorem refssfne

Description: A cover is a refinement iff it is a subcover of something which is both finer and a refinement. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Hypotheses refssfne.1 ⊢ 𝑋 = ∪ 𝐴
refssfne.2 ⊢ 𝑌 = ∪ 𝐵
Assertion refssfne ( 𝑋 = 𝑌 → ( 𝐵 Ref 𝐴 ↔ ∃ 𝑐 ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 refssfne.1 ⊢ 𝑋 = ∪ 𝐴
2 refssfne.2 ⊢ 𝑌 = ∪ 𝐵
3 refrel ⊢ Rel Ref
4 3 brrelex2i ⊢ ( 𝐵 Ref 𝐴 → 𝐴 ∈ V )
5 4 adantl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → 𝐴 ∈ V )
6 3 brrelex1i ⊢ ( 𝐵 Ref 𝐴 → 𝐵 ∈ V )
7 6 adantl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → 𝐵 ∈ V )
8 unexg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
9 5 7 8 syl2anc ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
10 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
11 10 a1i ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) )
12 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
13 12 a1i ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) )
14 eqimss2 ⊢ ( 𝑋 = 𝑌 → 𝑌 ⊆ 𝑋 )
15 14 adantr ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → 𝑌 ⊆ 𝑋 )
16 ssequn2 ⊢ ( 𝑌 ⊆ 𝑋 ↔ ( 𝑋 ∪ 𝑌 ) = 𝑋 )
17 15 16 sylib ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( 𝑋 ∪ 𝑌 ) = 𝑋 )
18 17 eqcomd ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → 𝑋 = ( 𝑋 ∪ 𝑌 ) )
19 1 2 uneq12i ⊢ ( 𝑋 ∪ 𝑌 ) = ( ∪ 𝐴 ∪ ∪ 𝐵 )
20 uniun ⊢ ∪ ( 𝐴 ∪ 𝐵 ) = ( ∪ 𝐴 ∪ ∪ 𝐵 )
21 19 20 eqtr4i ⊢ ( 𝑋 ∪ 𝑌 ) = ∪ ( 𝐴 ∪ 𝐵 )
22 1 21 fness ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ V ∧ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ 𝑋 = ( 𝑋 ∪ 𝑌 ) ) → 𝐴 Fne ( 𝐴 ∪ 𝐵 ) )
23 9 13 18 22 syl3anc ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → 𝐴 Fne ( 𝐴 ∪ 𝐵 ) )
24 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
25 ssid ⊢ 𝑥 ⊆ 𝑥
26 sseq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑥 ) )
27 26 rspcev ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
28 25 27 mpan2 ⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
29 28 a1i ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
30 refssex ⊢ ( ( 𝐵 Ref 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
31 30 ex ⊢ ( 𝐵 Ref 𝐴 → ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
32 31 adantl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
33 29 32 jaod ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
34 24 33 biimtrid ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
35 34 ralrimiv ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
36 21 1 isref ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( ( 𝐴 ∪ 𝐵 ) Ref 𝐴 ↔ ( 𝑋 = ( 𝑋 ∪ 𝑌 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
37 9 36 syl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( ( 𝐴 ∪ 𝐵 ) Ref 𝐴 ↔ ( 𝑋 = ( 𝑋 ∪ 𝑌 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
38 18 35 37 mpbir2and ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( 𝐴 ∪ 𝐵 ) Ref 𝐴 )
39 11 23 38 jca32 ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 Fne ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) Ref 𝐴 ) ) )
40 sseq2 ⊢ ( 𝑐 = ( 𝐴 ∪ 𝐵 ) → ( 𝐵 ⊆ 𝑐 ↔ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ) )
41 breq2 ⊢ ( 𝑐 = ( 𝐴 ∪ 𝐵 ) → ( 𝐴 Fne 𝑐 ↔ 𝐴 Fne ( 𝐴 ∪ 𝐵 ) ) )
42 breq1 ⊢ ( 𝑐 = ( 𝐴 ∪ 𝐵 ) → ( 𝑐 Ref 𝐴 ↔ ( 𝐴 ∪ 𝐵 ) Ref 𝐴 ) )
43 41 42 anbi12d ⊢ ( 𝑐 = ( 𝐴 ∪ 𝐵 ) → ( ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ↔ ( 𝐴 Fne ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) Ref 𝐴 ) ) )
44 40 43 anbi12d ⊢ ( 𝑐 = ( 𝐴 ∪ 𝐵 ) → ( ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ↔ ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 Fne ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) Ref 𝐴 ) ) ) )
45 44 spcegv ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 Fne ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) Ref 𝐴 ) ) → ∃ 𝑐 ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )
46 9 39 45 sylc ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐵 Ref 𝐴 ) → ∃ 𝑐 ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) )
47 46 ex ⊢ ( 𝑋 = 𝑌 → ( 𝐵 Ref 𝐴 → ∃ 𝑐 ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )
48 vex ⊢ 𝑐 ∈ V
49 48 ssex ⊢ ( 𝐵 ⊆ 𝑐 → 𝐵 ∈ V )
50 49 ad2antrl ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝐵 ∈ V )
51 simprl ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝐵 ⊆ 𝑐 )
52 simpl ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑋 = 𝑌 )
53 eqid ⊢ ∪ 𝑐 = ∪ 𝑐
54 53 1 refbas ⊢ ( 𝑐 Ref 𝐴 → 𝑋 = ∪ 𝑐 )
55 54 adantl ⊢ ( ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) → 𝑋 = ∪ 𝑐 )
56 55 ad2antll ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑋 = ∪ 𝑐 )
57 52 56 eqtr3d ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑌 = ∪ 𝑐 )
58 2 53 ssref ⊢ ( ( 𝐵 ∈ V ∧ 𝐵 ⊆ 𝑐 ∧ 𝑌 = ∪ 𝑐 ) → 𝐵 Ref 𝑐 )
59 50 51 57 58 syl3anc ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝐵 Ref 𝑐 )
60 simprrr ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑐 Ref 𝐴 )
61 reftr ⊢ ( ( 𝐵 Ref 𝑐 ∧ 𝑐 Ref 𝐴 ) → 𝐵 Ref 𝐴 )
62 59 60 61 syl2anc ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝐵 Ref 𝐴 )
63 62 ex ⊢ ( 𝑋 = 𝑌 → ( ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) → 𝐵 Ref 𝐴 ) )
64 63 exlimdv ⊢ ( 𝑋 = 𝑌 → ( ∃ 𝑐 ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) → 𝐵 Ref 𝐴 ) )
65 47 64 impbid ⊢ ( 𝑋 = 𝑌 → ( 𝐵 Ref 𝐴 ↔ ∃ 𝑐 ( 𝐵 ⊆ 𝑐 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )