This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isf34lem5

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion isf34lem5 ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∩ 𝑋 ) = ∪ ( 𝐹 “ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2 imassrn ⊢ ( 𝐹 “ 𝑋 ) ⊆ ran 𝐹
3 1 isf34lem2 ⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
4 3 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
5 4 frnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ran 𝐹 ⊆ 𝒫 𝐴 )
6 2 5 sstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 )
7 simprl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ⊆ 𝒫 𝐴 )
8 4 fdmd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → dom 𝐹 = 𝒫 𝐴 )
9 7 8 sseqtrrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ⊆ dom 𝐹 )
10 sseqin2 ⊢ ( 𝑋 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑋 ) = 𝑋 )
11 9 10 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( dom 𝐹 ∩ 𝑋 ) = 𝑋 )
12 simprr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ≠ ∅ )
13 11 12 eqnetrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( dom 𝐹 ∩ 𝑋 ) ≠ ∅ )
14 imadisj ⊢ ( ( 𝐹 “ 𝑋 ) = ∅ ↔ ( dom 𝐹 ∩ 𝑋 ) = ∅ )
15 14 necon3bii ⊢ ( ( 𝐹 “ 𝑋 ) ≠ ∅ ↔ ( dom 𝐹 ∩ 𝑋 ) ≠ ∅ )
16 13 15 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 “ 𝑋 ) ≠ ∅ )
17 6 16 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 ∧ ( 𝐹 “ 𝑋 ) ≠ ∅ ) )
18 1 isf34lem4 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 ∧ ( 𝐹 “ 𝑋 ) ≠ ∅ ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) = ∩ ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) )
19 17 18 syldan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) = ∩ ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) )
20 1 isf34lem3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 )
21 20 adantrr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 )
22 21 inteqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ∩ ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = ∩ 𝑋 )
23 19 22 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) = ∩ 𝑋 )
24 23 fveq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ( 𝐹 ‘ ∩ 𝑋 ) )
25 1 compsscnv ⊢ ◡ 𝐹 = 𝐹
26 25 fveq1i ⊢ ( ◡ 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ( 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) )
27 1 compssiso ⊢ ( 𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) )
28 isof1o ⊢ ( 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) → 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 )
29 27 28 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 )
30 sspwuni ⊢ ( ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 ↔ ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 )
31 6 30 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 )
32 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 ↔ ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 ) )
33 32 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 ↔ ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 ) )
34 31 33 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 )
35 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 ∧ ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ∪ ( 𝐹 “ 𝑋 ) )
36 29 34 35 syl2an2r ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ∪ ( 𝐹 “ 𝑋 ) )
37 26 36 eqtr3id ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ∪ ( 𝐹 “ 𝑋 ) )
38 24 37 eqtr3d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∩ 𝑋 ) = ∪ ( 𝐹 “ 𝑋 ) )