Metamath Proof Explorer

Theorem pwfilem

Description: Lemma for pwfi . (Contributed by NM, 26-Mar-2007)

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 vex ⊢ c ∈ V
4 snex ⊢ x ∈ V
5 3 4 unex ⊢ c ∪ x ∈ V
6 5 1 fnmpti ⊢ F Fn 𝒫 b
7 dffn4 ⊢ F Fn 𝒫 b ↔ F : 𝒫 b ⟶ onto ran ⁡ F
8 6 7 mpbi ⊢ F : 𝒫 b ⟶ onto ran ⁡ F
9 fodomfi ⊢ 𝒫 b ∈ Fin ∧ F : 𝒫 b ⟶ onto ran ⁡ F → ran ⁡ F ≼ 𝒫 b
10 8 9 mpan2 ⊢ 𝒫 b ∈ Fin → ran ⁡ F ≼ 𝒫 b
11 domfi ⊢ 𝒫 b ∈ Fin ∧ ran ⁡ F ≼ 𝒫 b → ran ⁡ F ∈ Fin
12 10 11 mpdan ⊢ 𝒫 b ∈ Fin → ran ⁡ F ∈ Fin
13 eldifi ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → d ∈ 𝒫 b ∪ x
14 4 elpwun ⊢ d ∈ 𝒫 b ∪ x ↔ d ∖ x ∈ 𝒫 b
15 13 14 sylib ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → d ∖ x ∈ 𝒫 b
16 undif1 ⊢ d ∖ x ∪ x = d ∪ x
17 elpwunsn ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → x ∈ d
18 17 snssd ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → x ⊆ d
19 ssequn2 ⊢ x ⊆ d ↔ d ∪ x = d
20 18 19 sylib ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → d ∪ x = d
21 16 20 syl5req ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → d = d ∖ x ∪ x
22 uneq1 ⊢ c = d ∖ x → c ∪ x = d ∖ x ∪ x
23 22 rspceeqv ⊢ d ∖ x ∈ 𝒫 b ∧ d = d ∖ x ∪ x → ∃ c ∈ 𝒫 b d = c ∪ x
24 15 21 23 syl2anc ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → ∃ c ∈ 𝒫 b d = c ∪ x
25 1 5 elrnmpti ⊢ d ∈ ran ⁡ F ↔ ∃ c ∈ 𝒫 b d = c ∪ x
26 24 25 sylibr ⊢ d ∈ 𝒫 b ∪ x ∖ 𝒫 b → d ∈ ran ⁡ F
27 26 ssriv ⊢ 𝒫 b ∪ x ∖ 𝒫 b ⊆ ran ⁡ F
28 ssdomg ⊢ ran ⁡ F ∈ Fin → 𝒫 b ∪ x ∖ 𝒫 b ⊆ ran ⁡ F → 𝒫 b ∪ x ∖ 𝒫 b ≼ ran ⁡ F
29 12 27 28 mpisyl ⊢ 𝒫 b ∈ Fin → 𝒫 b ∪ x ∖ 𝒫 b ≼ ran ⁡ F
30 domfi ⊢ ran ⁡ F ∈ Fin ∧ 𝒫 b ∪ x ∖ 𝒫 b ≼ ran ⁡ F → 𝒫 b ∪ x ∖ 𝒫 b ∈ Fin
31 12 29 30 syl2anc ⊢ 𝒫 b ∈ Fin → 𝒫 b ∪ x ∖ 𝒫 b ∈ Fin
32 unfi ⊢ 𝒫 b ∪ x ∖ 𝒫 b ∈ Fin ∧ 𝒫 b ∈ Fin → 𝒫 b ∪ x ∖ 𝒫 b ∪ 𝒫 b ∈ Fin
33 31 32 mpancom ⊢ 𝒫 b ∈ Fin → 𝒫 b ∪ x ∖ 𝒫 b ∪ 𝒫 b ∈ Fin
34 2 33 eqeltrid ⊢ 𝒫 b ∈ Fin → 𝒫 b ∪ x ∈ Fin