Metamath Proof Explorer

Theorem findcard2OLD

Description: Obsolete version of findcard2 as of 6-Aug-2024. (Contributed by Jeff Madsen, 8-Jul-2010) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses findcard2OLD.1 ⊢x=∅→φ↔ψ
findcard2OLD.2 ⊢x=y→φ↔χ
findcard2OLD.3 ⊢x=y∪z→φ↔θ
findcard2OLD.4 ⊢x=A→φ↔τ
findcard2OLD.5 ⊢ψ
findcard2OLD.6 ⊢y∈Fin→χ→θ
Assertion findcard2OLD ⊢A∈Fin→τ

Proof

Step Hyp Ref Expression
1 findcard2OLD.1 ⊢x=∅→φ↔ψ
2 findcard2OLD.2 ⊢x=y→φ↔χ
3 findcard2OLD.3 ⊢x=y∪z→φ↔θ
4 findcard2OLD.4 ⊢x=A→φ↔τ
5 findcard2OLD.5 ⊢ψ
6 findcard2OLD.6 ⊢y∈Fin→χ→θ
7 isfi ⊢x∈Fin↔∃w∈ωx≈w
8 breq2 ⊢w=∅→x≈w↔x≈∅
9 8 imbi1d ⊢w=∅→x≈w→φ↔x≈∅→φ
10 9 albidv ⊢w=∅→∀xx≈w→φ↔∀xx≈∅→φ
11 breq2 ⊢w=v→x≈w↔x≈v
12 11 imbi1d ⊢w=v→x≈w→φ↔x≈v→φ
13 12 albidv ⊢w=v→∀xx≈w→φ↔∀xx≈v→φ
14 breq2 ⊢w=suc⁡v→x≈w↔x≈suc⁡v
15 14 imbi1d ⊢w=suc⁡v→x≈w→φ↔x≈suc⁡v→φ
16 15 albidv ⊢w=suc⁡v→∀xx≈w→φ↔∀xx≈suc⁡v→φ
17 en0 ⊢x≈∅↔x=∅
18 5 1 mpbiri ⊢x=∅→φ
19 17 18 sylbi ⊢x≈∅→φ
20 19 ax-gen ⊢∀xx≈∅→φ
21 nsuceq0 ⊢suc⁡v≠∅
22 breq1 ⊢w=∅→w≈suc⁡v↔∅≈suc⁡v
23 22 anbi2d ⊢w=∅→v∈ω∧w≈suc⁡v↔v∈ω∧∅≈suc⁡v
24 peano1 ⊢∅∈ω
25 peano2 ⊢v∈ω→suc⁡v∈ω
26 nneneq ⊢∅∈ω∧suc⁡v∈ω→∅≈suc⁡v↔∅=suc⁡v
27 24 25 26 sylancr ⊢v∈ω→∅≈suc⁡v↔∅=suc⁡v
28 27 biimpa ⊢v∈ω∧∅≈suc⁡v→∅=suc⁡v
29 28 eqcomd ⊢v∈ω∧∅≈suc⁡v→suc⁡v=∅
30 23 29 syl6bi ⊢w=∅→v∈ω∧w≈suc⁡v→suc⁡v=∅
31 30 com12 ⊢v∈ω∧w≈suc⁡v→w=∅→suc⁡v=∅
32 31 necon3d ⊢v∈ω∧w≈suc⁡v→suc⁡v≠∅→w≠∅
33 21 32 mpi ⊢v∈ω∧w≈suc⁡v→w≠∅
34 33 ex ⊢v∈ω→w≈suc⁡v→w≠∅
35 n0 ⊢w≠∅↔∃zz∈w
36 dif1enOLD ⊢v∈ω∧w≈suc⁡v∧z∈w→w∖z≈v
37 36 3expia ⊢v∈ω∧w≈suc⁡v→z∈w→w∖z≈v
38 snssi ⊢z∈w→z⊆w
39 uncom ⊢w∖z∪z=z∪w∖z
40 undif ⊢z⊆w↔z∪w∖z=w
41 40 biimpi ⊢z⊆w→z∪w∖z=w
42 39 41 eqtrid ⊢z⊆w→w∖z∪z=w
43 vex ⊢w∈V
44 43 difexi ⊢w∖z∈V
45 breq1 ⊢y=w∖z→y≈v↔w∖z≈v
46 45 anbi2d ⊢y=w∖z→v∈ω∧y≈v↔v∈ω∧w∖z≈v
47 uneq1 ⊢y=w∖z→y∪z=w∖z∪z
48 47 sbceq1d ⊢y=w∖z→[˙y∪z/x]˙φ↔[˙w∖z∪z/x]˙φ
49 48 imbi2d ⊢y=w∖z→∀xx≈v→φ→[˙y∪z/x]˙φ↔∀xx≈v→φ→[˙w∖z∪z/x]˙φ
50 46 49 imbi12d ⊢y=w∖z→v∈ω∧y≈v→∀xx≈v→φ→[˙y∪z/x]˙φ↔v∈ω∧w∖z≈v→∀xx≈v→φ→[˙w∖z∪z/x]˙φ
51 breq1 ⊢x=y→x≈v↔y≈v
52 51 2 imbi12d ⊢x=y→x≈v→φ↔y≈v→χ
53 52 spvv ⊢∀xx≈v→φ→y≈v→χ
54 rspe ⊢v∈ω∧y≈v→∃v∈ωy≈v
55 isfi ⊢y∈Fin↔∃v∈ωy≈v
56 54 55 sylibr ⊢v∈ω∧y≈v→y∈Fin
57 pm2.27 ⊢y≈v→y≈v→χ→χ
58 57 adantl ⊢v∈ω∧y≈v→y≈v→χ→χ
59 56 58 6 sylsyld ⊢v∈ω∧y≈v→y≈v→χ→θ
60 53 59 syl5 ⊢v∈ω∧y≈v→∀xx≈v→φ→θ
61 vex ⊢y∈V
62 snex ⊢z∈V
63 61 62 unex ⊢y∪z∈V
64 63 3 sbcie ⊢[˙y∪z/x]˙φ↔θ
65 60 64 syl6ibr ⊢v∈ω∧y≈v→∀xx≈v→φ→[˙y∪z/x]˙φ
66 44 50 65 vtocl ⊢v∈ω∧w∖z≈v→∀xx≈v→φ→[˙w∖z∪z/x]˙φ
67 dfsbcq ⊢w∖z∪z=w→[˙w∖z∪z/x]˙φ↔[˙w/x]˙φ
68 67 imbi2d ⊢w∖z∪z=w→∀xx≈v→φ→[˙w∖z∪z/x]˙φ↔∀xx≈v→φ→[˙w/x]˙φ
69 66 68 imbitrid ⊢w∖z∪z=w→v∈ω∧w∖z≈v→∀xx≈v→φ→[˙w/x]˙φ
70 38 42 69 3syl ⊢z∈w→v∈ω∧w∖z≈v→∀xx≈v→φ→[˙w/x]˙φ
71 70 expd ⊢z∈w→v∈ω→w∖z≈v→∀xx≈v→φ→[˙w/x]˙φ
72 71 com12 ⊢v∈ω→z∈w→w∖z≈v→∀xx≈v→φ→[˙w/x]˙φ
73 72 adantr ⊢v∈ω∧w≈suc⁡v→z∈w→w∖z≈v→∀xx≈v→φ→[˙w/x]˙φ
74 37 73 mpdd ⊢v∈ω∧w≈suc⁡v→z∈w→∀xx≈v→φ→[˙w/x]˙φ
75 74 exlimdv ⊢v∈ω∧w≈suc⁡v→∃zz∈w→∀xx≈v→φ→[˙w/x]˙φ
76 35 75 biimtrid ⊢v∈ω∧w≈suc⁡v→w≠∅→∀xx≈v→φ→[˙w/x]˙φ
77 76 ex ⊢v∈ω→w≈suc⁡v→w≠∅→∀xx≈v→φ→[˙w/x]˙φ
78 34 77 mpdd ⊢v∈ω→w≈suc⁡v→∀xx≈v→φ→[˙w/x]˙φ
79 78 com23 ⊢v∈ω→∀xx≈v→φ→w≈suc⁡v→[˙w/x]˙φ
80 79 alrimdv ⊢v∈ω→∀xx≈v→φ→∀ww≈suc⁡v→[˙w/x]˙φ
81 nfv ⊢Ⅎwx≈suc⁡v→φ
82 nfv ⊢Ⅎxw≈suc⁡v
83 nfsbc1v ⊢Ⅎx[˙w/x]˙φ
84 82 83 nfim ⊢Ⅎxw≈suc⁡v→[˙w/x]˙φ
85 breq1 ⊢x=w→x≈suc⁡v↔w≈suc⁡v
86 sbceq1a ⊢x=w→φ↔[˙w/x]˙φ
87 85 86 imbi12d ⊢x=w→x≈suc⁡v→φ↔w≈suc⁡v→[˙w/x]˙φ
88 81 84 87 cbvalv1 ⊢∀xx≈suc⁡v→φ↔∀ww≈suc⁡v→[˙w/x]˙φ
89 80 88 syl6ibr ⊢v∈ω→∀xx≈v→φ→∀xx≈suc⁡v→φ
90 10 13 16 20 89 finds1 ⊢w∈ω→∀xx≈w→φ
91 90 19.21bi ⊢w∈ω→x≈w→φ
92 91 rexlimiv ⊢∃w∈ωx≈w→φ
93 7 92 sylbi ⊢x∈Fin→φ
94 4 93 vtoclga ⊢A∈Fin→τ