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 ⊢ 𝑋 = ∪ 𝐴
fnessref.2 ⊢ 𝑌 = ∪ 𝐵
Assertion fnessref ( 𝑋 = 𝑌 → ( 𝐴 Fne 𝐵 ↔ ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 fnessref.1 ⊢ 𝑋 = ∪ 𝐴
2 fnessref.2 ⊢ 𝑌 = ∪ 𝐵
3 fnerel ⊢ Rel Fne
4 3 brrelex2i ⊢ ( 𝐴 Fne 𝐵 → 𝐵 ∈ V )
5 4 adantl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → 𝐵 ∈ V )
6 rabexg ⊢ ( 𝐵 ∈ V → { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ V )
7 5 6 syl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ V )
8 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ 𝐵
9 8 a1i ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ 𝐵 )
10 1 eleq2i ⊢ ( 𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝐴 )
11 eluni ⊢ ( 𝑡 ∈ ∪ 𝐴 ↔ ∃ 𝑧 ( 𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) )
12 10 11 bitri ⊢ ( 𝑡 ∈ 𝑋 ↔ ∃ 𝑧 ( 𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) )
13 fnessex ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧 ) )
14 13 3expia ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑧 → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧 ) ) )
15 14 adantll ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑧 → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧 ) ) )
16 sseq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑧 ) )
17 16 rspcev ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑧 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
18 17 ex ⊢ ( 𝑧 ∈ 𝐴 → ( 𝑥 ⊆ 𝑧 → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
19 18 adantl ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ⊆ 𝑧 → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
20 19 anim2d ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧 ) → ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
21 20 reximdv ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
22 15 21 syld ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑧 → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
23 22 ex ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( 𝑧 ∈ 𝐴 → ( 𝑡 ∈ 𝑧 → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) ) )
24 23 com23 ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( 𝑡 ∈ 𝑧 → ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) ) )
25 24 impd ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( ( 𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
26 25 exlimdv ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( ∃ 𝑧 ( 𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
27 12 26 biimtrid ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( 𝑡 ∈ 𝑋 → ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
28 elunirab ⊢ ( 𝑡 ∈ ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑡 ∈ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) )
29 27 28 imbitrrdi ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( 𝑡 ∈ 𝑋 → 𝑡 ∈ ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ) )
30 29 ssrdv ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → 𝑋 ⊆ ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )
31 8 unissi ⊢ ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ ∪ 𝐵
32 simpl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → 𝑋 = 𝑌 )
33 32 2 eqtr2di ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ∪ 𝐵 = 𝑋 )
34 31 33 sseqtrid ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ 𝑋 )
35 30 34 eqssd ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → 𝑋 = ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )
36 fnessex ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
37 36 3expb ⊢ ( ( 𝐴 Fne 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
38 37 adantll ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
39 simpl ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → 𝑤 ∈ 𝐵 )
40 39 a1i ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → 𝑤 ∈ 𝐵 ) )
41 sseq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑤 ⊆ 𝑦 ↔ 𝑤 ⊆ 𝑧 ) )
42 41 rspcev ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ⊆ 𝑧 ) → ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 )
43 42 expcom ⊢ ( 𝑤 ⊆ 𝑧 → ( 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 ) )
44 43 ad2antll ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 ) )
45 44 com12 ⊢ ( 𝑧 ∈ 𝐴 → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 ) )
46 45 ad2antrl ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 ) )
47 40 46 jcad ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → ( 𝑤 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 ) ) )
48 sseq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ⊆ 𝑦 ↔ 𝑤 ⊆ 𝑦 ) )
49 48 rexbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 ) )
50 49 elrab ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ↔ ( 𝑤 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦 ) )
51 47 50 imbitrrdi ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ) )
52 simpr ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
53 52 a1i ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
54 51 53 jcad ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) → ( 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
55 54 reximdv2 ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) → ∃ 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
56 38 55 mpd ⊢ ( ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧 ) ) → ∃ 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
57 56 ralrimivva ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ 𝑧 ∃ 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
58 eqid ⊢ ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } = ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 }
59 1 58 isfne2 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ V → ( 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ↔ ( 𝑋 = ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ 𝑧 ∃ 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
60 5 6 59 3syl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ↔ ( 𝑋 = ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑡 ∈ 𝑧 ∃ 𝑤 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ( 𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
61 35 57 60 mpbir2and ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )
62 sseq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑦 ) )
63 62 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦 ) )
64 63 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ↔ ( 𝑧 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦 ) )
65 sseq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑤 ) )
66 65 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦 ↔ ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
67 66 bilani ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦 ) → ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
68 67 a1i ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( ( 𝑧 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦 ) → ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) )
69 64 68 biimtrid ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } → ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) )
70 69 ralrimiv ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
71 58 1 isref ⊢ ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ V → ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 ↔ ( 𝑋 = ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) ) )
72 5 6 71 3syl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 ↔ ( 𝑋 = ∪ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) ) )
73 35 70 72 mpbir2and ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 )
74 9 61 73 jca32 ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ 𝐵 ∧ ( 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 ) ) )
75 sseq1 ⊢ ( 𝑐 = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } → ( 𝑐 ⊆ 𝐵 ↔ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ 𝐵 ) )
76 breq2 ⊢ ( 𝑐 = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } → ( 𝐴 Fne 𝑐 ↔ 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ) )
77 breq1 ⊢ ( 𝑐 = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } → ( 𝑐 Ref 𝐴 ↔ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 ) )
78 76 77 anbi12d ⊢ ( 𝑐 = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } → ( ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ↔ ( 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 ) ) )
79 75 78 anbi12d ⊢ ( 𝑐 = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } → ( ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ↔ ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ 𝐵 ∧ ( 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 ) ) ) )
80 79 spcegv ⊢ ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ V → ( ( { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ⊆ 𝐵 ∧ ( 𝐴 Fne { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∧ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } Ref 𝐴 ) ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )
81 7 74 80 sylc ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 Fne 𝐵 ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) )
82 81 ex ⊢ ( 𝑋 = 𝑌 → ( 𝐴 Fne 𝐵 → ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )
83 simprrl ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝐴 Fne 𝑐 )
84 eqid ⊢ ∪ 𝑐 = ∪ 𝑐
85 1 84 fnebas ⊢ ( 𝐴 Fne 𝑐 → 𝑋 = ∪ 𝑐 )
86 83 85 syl ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑋 = ∪ 𝑐 )
87 simpl ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑋 = 𝑌 )
88 86 87 eqtr3d ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → ∪ 𝑐 = 𝑌 )
89 88 2 eqtrdi ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → ∪ 𝑐 = ∪ 𝐵 )
90 vuniex ⊢ ∪ 𝑐 ∈ V
91 89 90 eqeltrrdi ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → ∪ 𝐵 ∈ V )
92 uniexb ⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
93 91 92 sylibr ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝐵 ∈ V )
94 simprl ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑐 ⊆ 𝐵 )
95 84 2 fness ⊢ ( ( 𝐵 ∈ V ∧ 𝑐 ⊆ 𝐵 ∧ ∪ 𝑐 = 𝑌 ) → 𝑐 Fne 𝐵 )
96 93 94 88 95 syl3anc ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝑐 Fne 𝐵 )
97 fnetr ⊢ ( ( 𝐴 Fne 𝑐 ∧ 𝑐 Fne 𝐵 ) → 𝐴 Fne 𝐵 )
98 83 96 97 syl2anc ⊢ ( ( 𝑋 = 𝑌 ∧ ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) → 𝐴 Fne 𝐵 )
99 98 ex ⊢ ( 𝑋 = 𝑌 → ( ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) → 𝐴 Fne 𝐵 ) )
100 99 exlimdv ⊢ ( 𝑋 = 𝑌 → ( ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) → 𝐴 Fne 𝐵 ) )
101 82 100 impbid ⊢ ( 𝑋 = 𝑌 → ( 𝐴 Fne 𝐵 ↔ ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ( 𝐴 Fne 𝑐 ∧ 𝑐 Ref 𝐴 ) ) ) )