Metamath Proof Explorer

Theorem fnejoin2

Description: Join of equivalence classes under the fineness relation-part two. (Contributed by Jeff Hankins, 8-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion fnejoin2 ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 ↔ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 unisng ⊢ ( 𝑋 ∈ 𝑉 → ∪ { 𝑋 } = 𝑋 )
2 1 eqcomd ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 = ∪ { 𝑋 } )
3 2 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → 𝑋 = ∪ { 𝑋 } )
4 iftrue ⊢ ( 𝑆 = ∅ → if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = { 𝑋 } )
5 4 unieqd ⊢ ( 𝑆 = ∅ → ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = ∪ { 𝑋 } )
6 5 eqeq2d ⊢ ( 𝑆 = ∅ → ( 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ↔ 𝑋 = ∪ { 𝑋 } ) )
7 3 6 syl5ibrcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑆 = ∅ → 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ) )
8 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
9 unieq ⊢ ( 𝑦 = 𝑥 → ∪ 𝑦 = ∪ 𝑥 )
10 9 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑥 ) )
11 10 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 = ∪ 𝑥 )
12 11 3adant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 = ∪ 𝑥 )
13 fnejoin1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 Fne if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) )
14 eqid ⊢ ∪ 𝑥 = ∪ 𝑥
15 eqid ⊢ ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 )
16 14 15 fnebas ⊢ ( 𝑥 Fne if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) → ∪ 𝑥 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) )
17 13 16 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → ∪ 𝑥 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) )
18 12 17 eqtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) )
19 18 3expia ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑥 ∈ 𝑆 → 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ) )
20 19 exlimdv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( ∃ 𝑥 𝑥 ∈ 𝑆 → 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ) )
21 8 20 biimtrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( 𝑆 ≠ ∅ → 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ) )
22 7 21 pm2.61dne ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) )
23 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
24 15 23 fnebas ⊢ ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 → ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = ∪ 𝑇 )
25 22 24 sylan9eq ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 ) → 𝑋 = ∪ 𝑇 )
26 25 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 → 𝑋 = ∪ 𝑇 ) )
27 fnetr ⊢ ( ( 𝑥 Fne if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ∧ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 ) → 𝑥 Fne 𝑇 )
28 27 ex ⊢ ( 𝑥 Fne if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 → 𝑥 Fne 𝑇 ) )
29 13 28 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝑥 ∈ 𝑆 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 → 𝑥 Fne 𝑇 ) )
30 29 3expa ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ 𝑥 ∈ 𝑆 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 → 𝑥 Fne 𝑇 ) )
31 30 ralrimdva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 → ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) )
32 26 31 jcad ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 → ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) )
33 22 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → 𝑋 = ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) )
34 simprl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → 𝑋 = ∪ 𝑇 )
35 33 34 eqtr3d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = ∪ 𝑇 )
36 sseq1 ⊢ ( { 𝑋 } = if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) → ( { 𝑋 } ⊆ ( topGen ‘ 𝑇 ) ↔ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ⊆ ( topGen ‘ 𝑇 ) ) )
37 sseq1 ⊢ ( ∪ 𝑆 = if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) → ( ∪ 𝑆 ⊆ ( topGen ‘ 𝑇 ) ↔ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ⊆ ( topGen ‘ 𝑇 ) ) )
38 elex ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
39 38 ad2antrr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → 𝑋 ∈ V )
40 34 39 eqeltrrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → ∪ 𝑇 ∈ V )
41 uniexb ⊢ ( 𝑇 ∈ V ↔ ∪ 𝑇 ∈ V )
42 40 41 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → 𝑇 ∈ V )
43 ssid ⊢ 𝑇 ⊆ 𝑇
44 eltg3i ⊢ ( ( 𝑇 ∈ V ∧ 𝑇 ⊆ 𝑇 ) → ∪ 𝑇 ∈ ( topGen ‘ 𝑇 ) )
45 42 43 44 sylancl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → ∪ 𝑇 ∈ ( topGen ‘ 𝑇 ) )
46 34 45 eqeltrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → 𝑋 ∈ ( topGen ‘ 𝑇 ) )
47 46 snssd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → { 𝑋 } ⊆ ( topGen ‘ 𝑇 ) )
48 47 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) ∧ 𝑆 = ∅ ) → { 𝑋 } ⊆ ( topGen ‘ 𝑇 ) )
49 simplrr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) ∧ ¬ 𝑆 = ∅ ) → ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 )
50 fnetg ⊢ ( 𝑥 Fne 𝑇 → 𝑥 ⊆ ( topGen ‘ 𝑇 ) )
51 50 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 → ∀ 𝑥 ∈ 𝑆 𝑥 ⊆ ( topGen ‘ 𝑇 ) )
52 49 51 syl ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) ∧ ¬ 𝑆 = ∅ ) → ∀ 𝑥 ∈ 𝑆 𝑥 ⊆ ( topGen ‘ 𝑇 ) )
53 unissb ⊢ ( ∪ 𝑆 ⊆ ( topGen ‘ 𝑇 ) ↔ ∀ 𝑥 ∈ 𝑆 𝑥 ⊆ ( topGen ‘ 𝑇 ) )
54 52 53 sylibr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) ∧ ¬ 𝑆 = ∅ ) → ∪ 𝑆 ⊆ ( topGen ‘ 𝑇 ) )
55 36 37 48 54 ifbothda ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ⊆ ( topGen ‘ 𝑇 ) )
56 15 23 isfne4 ⊢ ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 ↔ ( ∪ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) = ∪ 𝑇 ∧ if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) ⊆ ( topGen ‘ 𝑇 ) ) )
57 35 55 56 sylanbrc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) ∧ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) → if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 )
58 57 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) → if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 ) )
59 32 58 impbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ) → ( if ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) Fne 𝑇 ↔ ( 𝑋 = ∪ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 Fne 𝑇 ) ) )