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 ( ( 𝐴𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴𝑋 ≠ ∅ ) ) → ( 𝐹 𝑋 ) = ( 𝐹𝑋 ) )