Metamath Proof Explorer

Theorem pwfseqlem2

Description: Lemma for pwfseq . (Contributed by Mario Carneiro, 18-Nov-2014) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses pwfseqlem4.g ⊢ φ → G : 𝒫 A ⟶ 1-1 ⋃ n ∈ ω A n
pwfseqlem4.x ⊢ φ → X ⊆ A
pwfseqlem4.h ⊢ φ → H : ω ⟶ 1-1 onto X
pwfseqlem4.ps ⊢ ψ ↔ x ⊆ A ∧ r ⊆ x × x ∧ r We x ∧ ω ≼ x
pwfseqlem4.k ⊢ φ ∧ ψ → K : ⋃ n ∈ ω x n ⟶ 1-1 x
pwfseqlem4.d ⊢ D = G ⁡ w ∈ x | K -1 ⁡ w ∈ ran ⁡ G ∧ ¬ w ∈ G -1 ⁡ K -1 ⁡ w
pwfseqlem4.f ⊢ F = x ∈ V , r ∈ V ⟼ if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x
Assertion pwfseqlem2 ⊢ Y ∈ Fin ∧ R ∈ V → Y F R = H ⁡ card ⁡ Y

Proof

Step Hyp Ref Expression
1 pwfseqlem4.g ⊢ φ → G : 𝒫 A ⟶ 1-1 ⋃ n ∈ ω A n
2 pwfseqlem4.x ⊢ φ → X ⊆ A
3 pwfseqlem4.h ⊢ φ → H : ω ⟶ 1-1 onto X
4 pwfseqlem4.ps ⊢ ψ ↔ x ⊆ A ∧ r ⊆ x × x ∧ r We x ∧ ω ≼ x
5 pwfseqlem4.k ⊢ φ ∧ ψ → K : ⋃ n ∈ ω x n ⟶ 1-1 x
6 pwfseqlem4.d ⊢ D = G ⁡ w ∈ x | K -1 ⁡ w ∈ ran ⁡ G ∧ ¬ w ∈ G -1 ⁡ K -1 ⁡ w
7 pwfseqlem4.f ⊢ F = x ∈ V , r ∈ V ⟼ if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x
8 oveq1 ⊢ a = Y → a F s = Y F s
9 2fveq3 ⊢ a = Y → H ⁡ card ⁡ a = H ⁡ card ⁡ Y
10 8 9 eqeq12d ⊢ a = Y → a F s = H ⁡ card ⁡ a ↔ Y F s = H ⁡ card ⁡ Y
11 oveq2 ⊢ s = R → Y F s = Y F R
12 11 eqeq1d ⊢ s = R → Y F s = H ⁡ card ⁡ Y ↔ Y F R = H ⁡ card ⁡ Y
13 nfcv ⊢ Ⅎ _ x a
14 nfcv ⊢ Ⅎ _ r a
15 nfcv ⊢ Ⅎ _ r s
16 nfmpo1 ⊢ Ⅎ _ x x ∈ V , r ∈ V ⟼ if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x
17 7 16 nfcxfr ⊢ Ⅎ _ x F
18 nfcv ⊢ Ⅎ _ x r
19 13 17 18 nfov ⊢ Ⅎ _ x a F r
20 19 nfeq1 ⊢ Ⅎ x a F r = H ⁡ card ⁡ a
21 nfmpo2 ⊢ Ⅎ _ r x ∈ V , r ∈ V ⟼ if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x
22 7 21 nfcxfr ⊢ Ⅎ _ r F
23 14 22 15 nfov ⊢ Ⅎ _ r a F s
24 23 nfeq1 ⊢ Ⅎ r a F s = H ⁡ card ⁡ a
25 oveq1 ⊢ x = a → x F r = a F r
26 2fveq3 ⊢ x = a → H ⁡ card ⁡ x = H ⁡ card ⁡ a
27 25 26 eqeq12d ⊢ x = a → x F r = H ⁡ card ⁡ x ↔ a F r = H ⁡ card ⁡ a
28 oveq2 ⊢ r = s → a F r = a F s
29 28 eqeq1d ⊢ r = s → a F r = H ⁡ card ⁡ a ↔ a F s = H ⁡ card ⁡ a
30 vex ⊢ x ∈ V
31 vex ⊢ r ∈ V
32 fvex ⊢ H ⁡ card ⁡ x ∈ V
33 fvex ⊢ D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x ∈ V
34 32 33 ifex ⊢ if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x ∈ V
35 7 ovmpt4g ⊢ x ∈ V ∧ r ∈ V ∧ if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x ∈ V → x F r = if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x
36 30 31 34 35 mp3an ⊢ x F r = if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x
37 iftrue ⊢ x ∈ Fin → if x ∈ Fin H ⁡ card ⁡ x D ⁡ ⋂ z ∈ ω | ¬ D ⁡ z ∈ x = H ⁡ card ⁡ x
38 36 37 syl5eq ⊢ x ∈ Fin → x F r = H ⁡ card ⁡ x
39 38 adantr ⊢ x ∈ Fin ∧ r ∈ V → x F r = H ⁡ card ⁡ x
40 13 14 15 20 24 27 29 39 vtocl2gaf ⊢ a ∈ Fin ∧ s ∈ V → a F s = H ⁡ card ⁡ a
41 10 12 40 vtocl2ga ⊢ Y ∈ Fin ∧ R ∈ V → Y F R = H ⁡ card ⁡ Y