# Metamath Proof Explorer

## Theorem fnessref

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

Ref Expression
Hypotheses fnessref.1 ${⊢}{X}=\bigcup {A}$
fnessref.2 ${⊢}{Y}=\bigcup {B}$
Assertion fnessref ${⊢}{X}={Y}\to \left({A}\mathrm{Fne}{B}↔\exists {c}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 fnessref.1 ${⊢}{X}=\bigcup {A}$
2 fnessref.2 ${⊢}{Y}=\bigcup {B}$
3 fnerel ${⊢}\mathrm{Rel}\mathrm{Fne}$
4 3 brrelex2i ${⊢}{A}\mathrm{Fne}{B}\to {B}\in \mathrm{V}$
5 4 adantl ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to {B}\in \mathrm{V}$
6 rabexg ${⊢}{B}\in \mathrm{V}\to \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\in \mathrm{V}$
7 5 6 syl ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\in \mathrm{V}$
8 ssrab2 ${⊢}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq {B}$
9 8 a1i ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq {B}$
10 1 eleq2i ${⊢}{t}\in {X}↔{t}\in \bigcup {A}$
11 eluni ${⊢}{t}\in \bigcup {A}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({t}\in {z}\wedge {z}\in {A}\right)$
12 10 11 bitri ${⊢}{t}\in {X}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({t}\in {z}\wedge {z}\in {A}\right)$
13 fnessex ${⊢}\left({A}\mathrm{Fne}{B}\wedge {z}\in {A}\wedge {t}\in {z}\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge {x}\subseteq {z}\right)$
14 13 3expia ${⊢}\left({A}\mathrm{Fne}{B}\wedge {z}\in {A}\right)\to \left({t}\in {z}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge {x}\subseteq {z}\right)\right)$
15 14 adantll ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge {z}\in {A}\right)\to \left({t}\in {z}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge {x}\subseteq {z}\right)\right)$
16 sseq2 ${⊢}{y}={z}\to \left({x}\subseteq {y}↔{x}\subseteq {z}\right)$
17 16 rspcev ${⊢}\left({z}\in {A}\wedge {x}\subseteq {z}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}$
18 17 ex ${⊢}{z}\in {A}\to \left({x}\subseteq {z}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$
19 18 adantl ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge {z}\in {A}\right)\to \left({x}\subseteq {z}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$
20 19 anim2d ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge {z}\in {A}\right)\to \left(\left({t}\in {x}\wedge {x}\subseteq {z}\right)\to \left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)$
21 20 reximdv ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge {z}\in {A}\right)\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge {x}\subseteq {z}\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)$
22 15 21 syld ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge {z}\in {A}\right)\to \left({t}\in {z}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)$
23 22 ex ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left({z}\in {A}\to \left({t}\in {z}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)\right)$
24 23 com23 ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left({t}\in {z}\to \left({z}\in {A}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)\right)$
25 24 impd ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left(\left({t}\in {z}\wedge {z}\in {A}\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)$
26 25 exlimdv ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({t}\in {z}\wedge {z}\in {A}\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)$
27 12 26 syl5bi ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left({t}\in {X}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)$
28 elunirab ${⊢}{t}\in \bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {x}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$
29 27 28 syl6ibr ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left({t}\in {X}\to {t}\in \bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\right)$
30 29 ssrdv ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to {X}\subseteq \bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}$
31 8 unissi ${⊢}\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq \bigcup {B}$
32 simpl ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to {X}={Y}$
33 32 2 syl6req ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \bigcup {B}={X}$
34 31 33 sseqtrid ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq {X}$
35 30 34 eqssd ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to {X}=\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}$
36 fnessex ${⊢}\left({A}\mathrm{Fne}{B}\wedge {z}\in {A}\wedge {t}\in {z}\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)$
37 36 3expb ${⊢}\left({A}\mathrm{Fne}{B}\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)$
38 37 adantll ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)$
39 simpl ${⊢}\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to {w}\in {B}$
40 39 a1i ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \left(\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to {w}\in {B}\right)$
41 sseq2 ${⊢}{y}={z}\to \left({w}\subseteq {y}↔{w}\subseteq {z}\right)$
42 41 rspcev ${⊢}\left({z}\in {A}\wedge {w}\subseteq {z}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}$
43 42 expcom ${⊢}{w}\subseteq {z}\to \left({z}\in {A}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}\right)$
44 43 ad2antll ${⊢}\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to \left({z}\in {A}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}\right)$
45 44 com12 ${⊢}{z}\in {A}\to \left(\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}\right)$
46 45 ad2antrl ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \left(\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}\right)$
47 40 46 jcad ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \left(\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to \left({w}\in {B}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}\right)\right)$
48 sseq1 ${⊢}{x}={w}\to \left({x}\subseteq {y}↔{w}\subseteq {y}\right)$
49 48 rexbidv ${⊢}{x}={w}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}\right)$
50 49 elrab ${⊢}{w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}↔\left({w}\in {B}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\subseteq {y}\right)$
51 47 50 syl6ibr ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \left(\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to {w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\right)$
52 simpr ${⊢}\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to \left({t}\in {w}\wedge {w}\subseteq {z}\right)$
53 52 a1i ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \left(\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)$
54 51 53 jcad ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \left(\left({w}\in {B}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\to \left({w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
55 54 reximdv2 ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)\to \exists {w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)$
56 38 55 mpd ${⊢}\left(\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\wedge \left({z}\in {A}\wedge {t}\in {z}\right)\right)\to \exists {w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)$
57 56 ralrimivva ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {z}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)$
58 eqid ${⊢}\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}=\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}$
59 1 58 isfne2 ${⊢}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\in \mathrm{V}\to \left({A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}↔\left({X}=\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {z}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
60 5 6 59 3syl ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left({A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}↔\left({X}=\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {t}\in {z}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
61 35 57 60 mpbir2and ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to {A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}$
62 sseq1 ${⊢}{x}={z}\to \left({x}\subseteq {y}↔{z}\subseteq {y}\right)$
63 62 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}\right)$
64 63 elrab ${⊢}{z}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}↔\left({z}\in {B}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}\right)$
65 sseq2 ${⊢}{y}={w}\to \left({z}\subseteq {y}↔{z}\subseteq {w}\right)$
66 65 cbvrexvw ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}$
67 66 biimpi ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}\to \exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}$
68 67 adantl ${⊢}\left({z}\in {B}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}\right)\to \exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}$
69 68 a1i ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left(\left({z}\in {B}\wedge \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}\right)\to \exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)$
70 64 69 syl5bi ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left({z}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\to \exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)$
71 70 ralrimiv ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \forall {z}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}$
72 58 1 isref ${⊢}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\in \mathrm{V}\to \left(\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}↔\left({X}=\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \forall {z}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)$
73 5 6 72 3syl ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left(\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}↔\left({X}=\bigcup \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \forall {z}\in \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)$
74 35 71 73 mpbir2and ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}$
75 9 61 74 jca32 ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \left(\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq {B}\wedge \left({A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}\right)\right)$
76 sseq1 ${⊢}{c}=\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\to \left({c}\subseteq {B}↔\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq {B}\right)$
77 breq2 ${⊢}{c}=\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\to \left({A}\mathrm{Fne}{c}↔{A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\right)$
78 breq1 ${⊢}{c}=\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\to \left({c}\mathrm{Ref}{A}↔\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}\right)$
79 77 78 anbi12d ${⊢}{c}=\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\to \left(\left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)↔\left({A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}\right)\right)$
80 76 79 anbi12d ${⊢}{c}=\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\to \left(\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)↔\left(\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq {B}\wedge \left({A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}\right)\right)\right)$
81 80 spcegv ${⊢}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\in \mathrm{V}\to \left(\left(\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\subseteq {B}\wedge \left({A}\mathrm{Fne}\left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\wedge \left\{{x}\in {B}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right\}\mathrm{Ref}{A}\right)\right)\to \exists {c}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)$
82 7 75 81 sylc ${⊢}\left({X}={Y}\wedge {A}\mathrm{Fne}{B}\right)\to \exists {c}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)$
83 82 ex ${⊢}{X}={Y}\to \left({A}\mathrm{Fne}{B}\to \exists {c}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)$
84 simprrl ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to {A}\mathrm{Fne}{c}$
85 eqid ${⊢}\bigcup {c}=\bigcup {c}$
86 1 85 fnebas ${⊢}{A}\mathrm{Fne}{c}\to {X}=\bigcup {c}$
87 84 86 syl ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to {X}=\bigcup {c}$
88 simpl ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to {X}={Y}$
89 87 88 eqtr3d ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to \bigcup {c}={Y}$
90 89 2 syl6eq ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to \bigcup {c}=\bigcup {B}$
91 vuniex ${⊢}\bigcup {c}\in \mathrm{V}$
92 90 91 syl6eqelr ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to \bigcup {B}\in \mathrm{V}$
93 uniexb ${⊢}{B}\in \mathrm{V}↔\bigcup {B}\in \mathrm{V}$
94 92 93 sylibr ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to {B}\in \mathrm{V}$
95 simprl ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to {c}\subseteq {B}$
96 85 2 fness ${⊢}\left({B}\in \mathrm{V}\wedge {c}\subseteq {B}\wedge \bigcup {c}={Y}\right)\to {c}\mathrm{Fne}{B}$
97 94 95 89 96 syl3anc ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to {c}\mathrm{Fne}{B}$
98 fnetr ${⊢}\left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Fne}{B}\right)\to {A}\mathrm{Fne}{B}$
99 84 97 98 syl2anc ${⊢}\left({X}={Y}\wedge \left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)\to {A}\mathrm{Fne}{B}$
100 99 ex ${⊢}{X}={Y}\to \left(\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\to {A}\mathrm{Fne}{B}\right)$
101 100 exlimdv ${⊢}{X}={Y}\to \left(\exists {c}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\to {A}\mathrm{Fne}{B}\right)$
102 83 101 impbid ${⊢}{X}={Y}\to \left({A}\mathrm{Fne}{B}↔\exists {c}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {B}\wedge \left({A}\mathrm{Fne}{c}\wedge {c}\mathrm{Ref}{A}\right)\right)\right)$