Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  refssfne Structured version   Visualization version   GIF version

Theorem refssfne 32892
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.)
Hypotheses
Ref Expression
refssfne.1 𝑋 = 𝐴
refssfne.2 𝑌 = 𝐵
Assertion
Ref Expression
refssfne (𝑋 = 𝑌 → (𝐵Ref𝐴 ↔ ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))))
Distinct variable groups:   𝐴,𝑐   𝐵,𝑐   𝑋,𝑐   𝑌,𝑐

Proof of Theorem refssfne
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 refrel 21683 . . . . . . 7 Rel Ref
21brrelex2i 5395 . . . . . 6 (𝐵Ref𝐴𝐴 ∈ V)
32adantl 475 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐴 ∈ V)
41brrelex1i 5394 . . . . . 6 (𝐵Ref𝐴𝐵 ∈ V)
54adantl 475 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐵 ∈ V)
6 unexg 7220 . . . . 5 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
73, 5, 6syl2anc 581 . . . 4 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝐴𝐵) ∈ V)
8 ssun2 4005 . . . . . 6 𝐵 ⊆ (𝐴𝐵)
98a1i 11 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐵 ⊆ (𝐴𝐵))
10 ssun1 4004 . . . . . . 7 𝐴 ⊆ (𝐴𝐵)
1110a1i 11 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐴 ⊆ (𝐴𝐵))
12 eqimss2 3884 . . . . . . . . 9 (𝑋 = 𝑌𝑌𝑋)
1312adantr 474 . . . . . . . 8 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝑌𝑋)
14 ssequn2 4014 . . . . . . . 8 (𝑌𝑋 ↔ (𝑋𝑌) = 𝑋)
1513, 14sylib 210 . . . . . . 7 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑋𝑌) = 𝑋)
1615eqcomd 2832 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝑋 = (𝑋𝑌))
17 refssfne.1 . . . . . . 7 𝑋 = 𝐴
18 refssfne.2 . . . . . . . . 9 𝑌 = 𝐵
1917, 18uneq12i 3993 . . . . . . . 8 (𝑋𝑌) = ( 𝐴 𝐵)
20 uniun 4680 . . . . . . . 8 (𝐴𝐵) = ( 𝐴 𝐵)
2119, 20eqtr4i 2853 . . . . . . 7 (𝑋𝑌) = (𝐴𝐵)
2217, 21fness 32883 . . . . . 6 (((𝐴𝐵) ∈ V ∧ 𝐴 ⊆ (𝐴𝐵) ∧ 𝑋 = (𝑋𝑌)) → 𝐴Fne(𝐴𝐵))
237, 11, 16, 22syl3anc 1496 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐴Fne(𝐴𝐵))
24 elun 3981 . . . . . . . 8 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
25 ssid 3849 . . . . . . . . . . 11 𝑥𝑥
26 sseq2 3853 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑥𝑦𝑥𝑥))
2726rspcev 3527 . . . . . . . . . . 11 ((𝑥𝐴𝑥𝑥) → ∃𝑦𝐴 𝑥𝑦)
2825, 27mpan2 684 . . . . . . . . . 10 (𝑥𝐴 → ∃𝑦𝐴 𝑥𝑦)
2928a1i 11 . . . . . . . . 9 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑥𝐴 → ∃𝑦𝐴 𝑥𝑦))
30 refssex 21686 . . . . . . . . . . 11 ((𝐵Ref𝐴𝑥𝐵) → ∃𝑦𝐴 𝑥𝑦)
3130ex 403 . . . . . . . . . 10 (𝐵Ref𝐴 → (𝑥𝐵 → ∃𝑦𝐴 𝑥𝑦))
3231adantl 475 . . . . . . . . 9 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑥𝐵 → ∃𝑦𝐴 𝑥𝑦))
3329, 32jaod 892 . . . . . . . 8 ((𝑋 = 𝑌𝐵Ref𝐴) → ((𝑥𝐴𝑥𝐵) → ∃𝑦𝐴 𝑥𝑦))
3424, 33syl5bi 234 . . . . . . 7 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑥 ∈ (𝐴𝐵) → ∃𝑦𝐴 𝑥𝑦))
3534ralrimiv 3175 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → ∀𝑥 ∈ (𝐴𝐵)∃𝑦𝐴 𝑥𝑦)
3621, 17isref 21684 . . . . . . 7 ((𝐴𝐵) ∈ V → ((𝐴𝐵)Ref𝐴 ↔ (𝑋 = (𝑋𝑌) ∧ ∀𝑥 ∈ (𝐴𝐵)∃𝑦𝐴 𝑥𝑦)))
377, 36syl 17 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → ((𝐴𝐵)Ref𝐴 ↔ (𝑋 = (𝑋𝑌) ∧ ∀𝑥 ∈ (𝐴𝐵)∃𝑦𝐴 𝑥𝑦)))
3816, 35, 37mpbir2and 706 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝐴𝐵)Ref𝐴)
399, 23, 38jca32 513 . . . 4 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝐵 ⊆ (𝐴𝐵) ∧ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴)))
40 sseq2 3853 . . . . . 6 (𝑐 = (𝐴𝐵) → (𝐵𝑐𝐵 ⊆ (𝐴𝐵)))
41 breq2 4878 . . . . . . 7 (𝑐 = (𝐴𝐵) → (𝐴Fne𝑐𝐴Fne(𝐴𝐵)))
42 breq1 4877 . . . . . . 7 (𝑐 = (𝐴𝐵) → (𝑐Ref𝐴 ↔ (𝐴𝐵)Ref𝐴))
4341, 42anbi12d 626 . . . . . 6 (𝑐 = (𝐴𝐵) → ((𝐴Fne𝑐𝑐Ref𝐴) ↔ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴)))
4440, 43anbi12d 626 . . . . 5 (𝑐 = (𝐴𝐵) → ((𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)) ↔ (𝐵 ⊆ (𝐴𝐵) ∧ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴))))
4544spcegv 3512 . . . 4 ((𝐴𝐵) ∈ V → ((𝐵 ⊆ (𝐴𝐵) ∧ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴)) → ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))))
467, 39, 45sylc 65 . . 3 ((𝑋 = 𝑌𝐵Ref𝐴) → ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)))
4746ex 403 . 2 (𝑋 = 𝑌 → (𝐵Ref𝐴 → ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))))
48 vex 3418 . . . . . . . 8 𝑐 ∈ V
4948ssex 5028 . . . . . . 7 (𝐵𝑐𝐵 ∈ V)
5049ad2antrl 721 . . . . . 6 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵 ∈ V)
51 simprl 789 . . . . . 6 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵𝑐)
52 simpl 476 . . . . . . 7 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑋 = 𝑌)
53 eqid 2826 . . . . . . . . . 10 𝑐 = 𝑐
5453, 17refbas 21685 . . . . . . . . 9 (𝑐Ref𝐴𝑋 = 𝑐)
5554adantl 475 . . . . . . . 8 ((𝐴Fne𝑐𝑐Ref𝐴) → 𝑋 = 𝑐)
5655ad2antll 722 . . . . . . 7 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑋 = 𝑐)
5752, 56eqtr3d 2864 . . . . . 6 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑌 = 𝑐)
5818, 53ssref 21687 . . . . . 6 ((𝐵 ∈ V ∧ 𝐵𝑐𝑌 = 𝑐) → 𝐵Ref𝑐)
5950, 51, 57, 58syl3anc 1496 . . . . 5 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵Ref𝑐)
60 simprrr 802 . . . . 5 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑐Ref𝐴)
61 reftr 21689 . . . . 5 ((𝐵Ref𝑐𝑐Ref𝐴) → 𝐵Ref𝐴)
6259, 60, 61syl2anc 581 . . . 4 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵Ref𝐴)
6362ex 403 . . 3 (𝑋 = 𝑌 → ((𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)) → 𝐵Ref𝐴))
6463exlimdv 2034 . 2 (𝑋 = 𝑌 → (∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)) → 𝐵Ref𝐴))
6547, 64impbid 204 1 (𝑋 = 𝑌 → (𝐵Ref𝐴 ↔ ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wo 880   = wceq 1658  wex 1880  wcel 2166  wral 3118  wrex 3119  Vcvv 3415  cun 3797  wss 3799   cuni 4659   class class class wbr 4874  Refcref 21677  Fnecfne 32870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-iota 6087  df-fun 6126  df-fv 6132  df-topgen 16458  df-ref 21680  df-fne 32871
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator