Metamath Proof Explorer


Theorem isf32lem8

Description: Lemma for isfin3-2 . K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014)

Ref Expression
Hypotheses isf32lem.a φF:ω𝒫G
isf32lem.b φxωFsucxFx
isf32lem.c φ¬ranFranF
isf32lem.d S=yω|FsucyFy
isf32lem.e J=uωιvS|vSu
isf32lem.f K=wSFwFsucwJ
Assertion isf32lem8 φAωKAG

Proof

Step Hyp Ref Expression
1 isf32lem.a φF:ω𝒫G
2 isf32lem.b φxωFsucxFx
3 isf32lem.c φ¬ranFranF
4 isf32lem.d S=yω|FsucyFy
5 isf32lem.e J=uωιvS|vSu
6 isf32lem.f K=wSFwFsucwJ
7 6 fveq1i KA=wSFwFsucwJA
8 4 ssrab3 Sω
9 1 2 3 4 isf32lem5 φ¬SFin
10 5 fin23lem22 Sω¬SFinJ:ω1-1 ontoS
11 8 9 10 sylancr φJ:ω1-1 ontoS
12 f1of J:ω1-1 ontoSJ:ωS
13 11 12 syl φJ:ωS
14 fvco3 J:ωSAωwSFwFsucwJA=wSFwFsucwJA
15 13 14 sylan φAωwSFwFsucwJA=wSFwFsucwJA
16 13 ffvelrnda φAωJAS
17 fveq2 w=JAFw=FJA
18 suceq w=JAsucw=sucJA
19 18 fveq2d w=JAFsucw=FsucJA
20 17 19 difeq12d w=JAFwFsucw=FJAFsucJA
21 eqid wSFwFsucw=wSFwFsucw
22 fvex FJAV
23 22 difexi FJAFsucJAV
24 20 21 23 fvmpt JASwSFwFsucwJA=FJAFsucJA
25 16 24 syl φAωwSFwFsucwJA=FJAFsucJA
26 15 25 eqtrd φAωwSFwFsucwJA=FJAFsucJA
27 7 26 eqtrid φAωKA=FJAFsucJA
28 1 adantr φAωF:ω𝒫G
29 8 16 sselid φAωJAω
30 28 29 ffvelrnd φAωFJA𝒫G
31 30 elpwid φAωFJAG
32 31 ssdifssd φAωFJAFsucJAG
33 27 32 eqsstrd φAωKAG