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 vsnex ⊢ 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