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 ( 𝑆 = ∅ , { 𝑋 } , ∪ 𝑆 ) )