Metamath Proof Explorer


Theorem fnejoin1

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

Ref Expression
Assertion fnejoin1 ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝐴 Fne if ( 𝑆 = ∅ , { 𝑋 } , 𝑆 ) )

Proof

Step Hyp Ref Expression
1 elssuni ( 𝐴𝑆𝐴 𝑆 )
2 1 3ad2ant3 ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝐴 𝑆 )
3 2 unissd ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝐴 𝑆 )
4 eqimss2 ( 𝑋 = 𝑦 𝑦𝑋 )
5 sspwuni ( 𝑦 ⊆ 𝒫 𝑋 𝑦𝑋 )
6 4 5 sylibr ( 𝑋 = 𝑦𝑦 ⊆ 𝒫 𝑋 )
7 6 ralimi ( ∀ 𝑦𝑆 𝑋 = 𝑦 → ∀ 𝑦𝑆 𝑦 ⊆ 𝒫 𝑋 )
8 7 3ad2ant2 ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → ∀ 𝑦𝑆 𝑦 ⊆ 𝒫 𝑋 )
9 unissb ( 𝑆 ⊆ 𝒫 𝑋 ↔ ∀ 𝑦𝑆 𝑦 ⊆ 𝒫 𝑋 )
10 8 9 sylibr ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑆 ⊆ 𝒫 𝑋 )
11 sspwuni ( 𝑆 ⊆ 𝒫 𝑋 𝑆𝑋 )
12 10 11 sylib ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑆𝑋 )
13 unieq ( 𝑦 = 𝐴 𝑦 = 𝐴 )
14 13 eqeq2d ( 𝑦 = 𝐴 → ( 𝑋 = 𝑦𝑋 = 𝐴 ) )
15 14 rspccva ( ( ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑋 = 𝐴 )
16 15 3adant1 ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑋 = 𝐴 )
17 12 16 sseqtrd ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑆 𝐴 )
18 3 17 eqssd ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝐴 = 𝑆 )
19 pwexg ( 𝑋𝑉 → 𝒫 𝑋 ∈ V )
20 19 3ad2ant1 ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝒫 𝑋 ∈ V )
21 20 10 ssexd ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑆 ∈ V )
22 bastg ( 𝑆 ∈ V → 𝑆 ⊆ ( topGen ‘ 𝑆 ) )
23 21 22 syl ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑆 ⊆ ( topGen ‘ 𝑆 ) )
24 2 23 sstrd ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝐴 ⊆ ( topGen ‘ 𝑆 ) )
25 eqid 𝐴 = 𝐴
26 eqid 𝑆 = 𝑆
27 25 26 isfne4 ( 𝐴 Fne 𝑆 ↔ ( 𝐴 = 𝑆𝐴 ⊆ ( topGen ‘ 𝑆 ) ) )
28 18 24 27 sylanbrc ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝐴 Fne 𝑆 )
29 ne0i ( 𝐴𝑆𝑆 ≠ ∅ )
30 29 3ad2ant3 ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝑆 ≠ ∅ )
31 ifnefalse ( 𝑆 ≠ ∅ → if ( 𝑆 = ∅ , { 𝑋 } , 𝑆 ) = 𝑆 )
32 30 31 syl ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → if ( 𝑆 = ∅ , { 𝑋 } , 𝑆 ) = 𝑆 )
33 28 32 breqtrrd ( ( 𝑋𝑉 ∧ ∀ 𝑦𝑆 𝑋 = 𝑦𝐴𝑆 ) → 𝐴 Fne if ( 𝑆 = ∅ , { 𝑋 } , 𝑆 ) )