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 34588
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 22700 . . . . . . 7 Rel Ref
21brrelex2i 5651 . . . . . 6 (𝐵Ref𝐴𝐴 ∈ V)
32adantl 483 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐴 ∈ V)
41brrelex1i 5650 . . . . . 6 (𝐵Ref𝐴𝐵 ∈ V)
54adantl 483 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐵 ∈ V)
6 unexg 7627 . . . . 5 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
73, 5, 6syl2anc 585 . . . 4 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝐴𝐵) ∈ V)
8 ssun2 4113 . . . . . 6 𝐵 ⊆ (𝐴𝐵)
98a1i 11 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐵 ⊆ (𝐴𝐵))
10 ssun1 4112 . . . . . . 7 𝐴 ⊆ (𝐴𝐵)
1110a1i 11 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐴 ⊆ (𝐴𝐵))
12 eqimss2 3983 . . . . . . . . 9 (𝑋 = 𝑌𝑌𝑋)
1312adantr 482 . . . . . . . 8 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝑌𝑋)
14 ssequn2 4123 . . . . . . . 8 (𝑌𝑋 ↔ (𝑋𝑌) = 𝑋)
1513, 14sylib 217 . . . . . . 7 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑋𝑌) = 𝑋)
1615eqcomd 2742 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝑋 = (𝑋𝑌))
17 refssfne.1 . . . . . . 7 𝑋 = 𝐴
18 refssfne.2 . . . . . . . . 9 𝑌 = 𝐵
1917, 18uneq12i 4101 . . . . . . . 8 (𝑋𝑌) = ( 𝐴 𝐵)
20 uniun 4870 . . . . . . . 8 (𝐴𝐵) = ( 𝐴 𝐵)
2119, 20eqtr4i 2767 . . . . . . 7 (𝑋𝑌) = (𝐴𝐵)
2217, 21fness 34579 . . . . . 6 (((𝐴𝐵) ∈ V ∧ 𝐴 ⊆ (𝐴𝐵) ∧ 𝑋 = (𝑋𝑌)) → 𝐴Fne(𝐴𝐵))
237, 11, 16, 22syl3anc 1371 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → 𝐴Fne(𝐴𝐵))
24 elun 4089 . . . . . . . 8 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
25 ssid 3948 . . . . . . . . . . 11 𝑥𝑥
26 sseq2 3952 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑥𝑦𝑥𝑥))
2726rspcev 3566 . . . . . . . . . . 11 ((𝑥𝐴𝑥𝑥) → ∃𝑦𝐴 𝑥𝑦)
2825, 27mpan2 689 . . . . . . . . . 10 (𝑥𝐴 → ∃𝑦𝐴 𝑥𝑦)
2928a1i 11 . . . . . . . . 9 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑥𝐴 → ∃𝑦𝐴 𝑥𝑦))
30 refssex 22703 . . . . . . . . . . 11 ((𝐵Ref𝐴𝑥𝐵) → ∃𝑦𝐴 𝑥𝑦)
3130ex 414 . . . . . . . . . 10 (𝐵Ref𝐴 → (𝑥𝐵 → ∃𝑦𝐴 𝑥𝑦))
3231adantl 483 . . . . . . . . 9 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑥𝐵 → ∃𝑦𝐴 𝑥𝑦))
3329, 32jaod 857 . . . . . . . 8 ((𝑋 = 𝑌𝐵Ref𝐴) → ((𝑥𝐴𝑥𝐵) → ∃𝑦𝐴 𝑥𝑦))
3424, 33syl5bi 243 . . . . . . 7 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝑥 ∈ (𝐴𝐵) → ∃𝑦𝐴 𝑥𝑦))
3534ralrimiv 3139 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → ∀𝑥 ∈ (𝐴𝐵)∃𝑦𝐴 𝑥𝑦)
3621, 17isref 22701 . . . . . . 7 ((𝐴𝐵) ∈ V → ((𝐴𝐵)Ref𝐴 ↔ (𝑋 = (𝑋𝑌) ∧ ∀𝑥 ∈ (𝐴𝐵)∃𝑦𝐴 𝑥𝑦)))
377, 36syl 17 . . . . . 6 ((𝑋 = 𝑌𝐵Ref𝐴) → ((𝐴𝐵)Ref𝐴 ↔ (𝑋 = (𝑋𝑌) ∧ ∀𝑥 ∈ (𝐴𝐵)∃𝑦𝐴 𝑥𝑦)))
3816, 35, 37mpbir2and 711 . . . . 5 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝐴𝐵)Ref𝐴)
399, 23, 38jca32 517 . . . 4 ((𝑋 = 𝑌𝐵Ref𝐴) → (𝐵 ⊆ (𝐴𝐵) ∧ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴)))
40 sseq2 3952 . . . . . 6 (𝑐 = (𝐴𝐵) → (𝐵𝑐𝐵 ⊆ (𝐴𝐵)))
41 breq2 5085 . . . . . . 7 (𝑐 = (𝐴𝐵) → (𝐴Fne𝑐𝐴Fne(𝐴𝐵)))
42 breq1 5084 . . . . . . 7 (𝑐 = (𝐴𝐵) → (𝑐Ref𝐴 ↔ (𝐴𝐵)Ref𝐴))
4341, 42anbi12d 632 . . . . . 6 (𝑐 = (𝐴𝐵) → ((𝐴Fne𝑐𝑐Ref𝐴) ↔ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴)))
4440, 43anbi12d 632 . . . . 5 (𝑐 = (𝐴𝐵) → ((𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)) ↔ (𝐵 ⊆ (𝐴𝐵) ∧ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴))))
4544spcegv 3541 . . . 4 ((𝐴𝐵) ∈ V → ((𝐵 ⊆ (𝐴𝐵) ∧ (𝐴Fne(𝐴𝐵) ∧ (𝐴𝐵)Ref𝐴)) → ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))))
467, 39, 45sylc 65 . . 3 ((𝑋 = 𝑌𝐵Ref𝐴) → ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)))
4746ex 414 . 2 (𝑋 = 𝑌 → (𝐵Ref𝐴 → ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))))
48 vex 3441 . . . . . . . 8 𝑐 ∈ V
4948ssex 5254 . . . . . . 7 (𝐵𝑐𝐵 ∈ V)
5049ad2antrl 726 . . . . . 6 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵 ∈ V)
51 simprl 769 . . . . . 6 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵𝑐)
52 simpl 484 . . . . . . 7 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑋 = 𝑌)
53 eqid 2736 . . . . . . . . . 10 𝑐 = 𝑐
5453, 17refbas 22702 . . . . . . . . 9 (𝑐Ref𝐴𝑋 = 𝑐)
5554adantl 483 . . . . . . . 8 ((𝐴Fne𝑐𝑐Ref𝐴) → 𝑋 = 𝑐)
5655ad2antll 727 . . . . . . 7 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑋 = 𝑐)
5752, 56eqtr3d 2778 . . . . . 6 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑌 = 𝑐)
5818, 53ssref 22704 . . . . . 6 ((𝐵 ∈ V ∧ 𝐵𝑐𝑌 = 𝑐) → 𝐵Ref𝑐)
5950, 51, 57, 58syl3anc 1371 . . . . 5 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵Ref𝑐)
60 simprrr 780 . . . . 5 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝑐Ref𝐴)
61 reftr 22706 . . . . 5 ((𝐵Ref𝑐𝑐Ref𝐴) → 𝐵Ref𝐴)
6259, 60, 61syl2anc 585 . . . 4 ((𝑋 = 𝑌 ∧ (𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))) → 𝐵Ref𝐴)
6362ex 414 . . 3 (𝑋 = 𝑌 → ((𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)) → 𝐵Ref𝐴))
6463exlimdv 1934 . 2 (𝑋 = 𝑌 → (∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴)) → 𝐵Ref𝐴))
6547, 64impbid 211 1 (𝑋 = 𝑌 → (𝐵Ref𝐴 ↔ ∃𝑐(𝐵𝑐 ∧ (𝐴Fne𝑐𝑐Ref𝐴))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 845   = wceq 1539  wex 1779  wcel 2104  wral 3062  wrex 3071  Vcvv 3437  cun 3890  wss 3892   cuni 4844   class class class wbr 5081  Refcref 22694  Fnecfne 34566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5496  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-iota 6406  df-fun 6456  df-fv 6462  df-topgen 17195  df-ref 22697  df-fne 34567
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator