Metamath Proof Explorer


Theorem pwfilem

Description: Lemma for pwfi . (Contributed by NM, 26-Mar-2007) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

Ref Expression
Hypothesis pwfilem.1 F = c 𝒫 b c x
Assertion pwfilem 𝒫 b Fin 𝒫 b x Fin

Proof

Step Hyp Ref Expression
1 pwfilem.1 F = c 𝒫 b c x
2 pwundif 𝒫 b x = 𝒫 b x 𝒫 b 𝒫 b
3 1 funmpt2 Fun F
4 vex c V
5 snex x V
6 4 5 unex c x V
7 6 1 dmmpti dom F = 𝒫 b
8 7 imaeq2i F dom F = F 𝒫 b
9 imadmrn F dom F = ran F
10 8 9 eqtr3i F 𝒫 b = ran F
11 imafi Fun F 𝒫 b Fin F 𝒫 b Fin
12 10 11 eqeltrrid Fun F 𝒫 b Fin ran F Fin
13 3 12 mpan 𝒫 b Fin ran F Fin
14 eldifi d 𝒫 b x 𝒫 b d 𝒫 b x
15 5 elpwun d 𝒫 b x d x 𝒫 b
16 14 15 sylib d 𝒫 b x 𝒫 b d x 𝒫 b
17 undif1 d x x = d x
18 elpwunsn d 𝒫 b x 𝒫 b x d
19 18 snssd d 𝒫 b x 𝒫 b x d
20 ssequn2 x d d x = d
21 19 20 sylib d 𝒫 b x 𝒫 b d x = d
22 17 21 eqtr2id d 𝒫 b x 𝒫 b d = d x x
23 uneq1 c = d x c x = d x x
24 23 rspceeqv d x 𝒫 b d = d x x c 𝒫 b d = c x
25 16 22 24 syl2anc d 𝒫 b x 𝒫 b c 𝒫 b d = c x
26 1 25 14 elrnmptd d 𝒫 b x 𝒫 b d ran F
27 26 ssriv 𝒫 b x 𝒫 b ran F
28 ssfi ran F Fin 𝒫 b x 𝒫 b ran F 𝒫 b x 𝒫 b Fin
29 13 27 28 sylancl 𝒫 b Fin 𝒫 b x 𝒫 b Fin
30 unfi 𝒫 b x 𝒫 b Fin 𝒫 b Fin 𝒫 b x 𝒫 b 𝒫 b Fin
31 29 30 mpancom 𝒫 b Fin 𝒫 b x 𝒫 b 𝒫 b Fin
32 2 31 eqeltrid 𝒫 b Fin 𝒫 b x Fin