Metamath Proof Explorer

Theorem findcard3OLD

Description: Obsolete version of findcard3 as of 7-Jan-2025. (Contributed by Mario Carneiro, 13-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses findcard3OLD.1 ⊢x=y→φ↔χ
findcard3OLD.2 ⊢x=A→φ↔τ
findcard3OLD.3 ⊢y∈Fin→∀xx⊂y→φ→χ
Assertion findcard3OLD ⊢A∈Fin→τ

Proof

Step Hyp Ref Expression
1 findcard3OLD.1 ⊢x=y→φ↔χ
2 findcard3OLD.2 ⊢x=A→φ↔τ
3 findcard3OLD.3 ⊢y∈Fin→∀xx⊂y→φ→χ
4 isfi ⊢A∈Fin↔∃w∈ωA≈w
5 nnon ⊢w∈ω→w∈On
6 eleq1w ⊢w=z→w∈ω↔z∈ω
7 breq2 ⊢w=z→x≈w↔x≈z
8 7 imbi1d ⊢w=z→x≈w→φ↔x≈z→φ
9 8 albidv ⊢w=z→∀xx≈w→φ↔∀xx≈z→φ
10 6 9 imbi12d ⊢w=z→w∈ω→∀xx≈w→φ↔z∈ω→∀xx≈z→φ
11 rspe ⊢w∈ω∧y≈w→∃w∈ωy≈w
12 isfi ⊢y∈Fin↔∃w∈ωy≈w
13 11 12 sylibr ⊢w∈ω∧y≈w→y∈Fin
14 19.21v ⊢∀xz∈ω→x≈z→φ↔z∈ω→∀xx≈z→φ
15 14 ralbii ⊢∀z∈w∀xz∈ω→x≈z→φ↔∀z∈wz∈ω→∀xx≈z→φ
16 ralcom4 ⊢∀z∈w∀xz∈ω→x≈z→φ↔∀x∀z∈wz∈ω→x≈z→φ
17 15 16 bitr3i ⊢∀z∈wz∈ω→∀xx≈z→φ↔∀x∀z∈wz∈ω→x≈z→φ
18 pssss ⊢x⊂y→x⊆y
19 ssfi ⊢y∈Fin∧x⊆y→x∈Fin
20 isfi ⊢x∈Fin↔∃z∈ωx≈z
21 19 20 sylib ⊢y∈Fin∧x⊆y→∃z∈ωx≈z
22 13 18 21 syl2an ⊢w∈ω∧y≈w∧x⊂y→∃z∈ωx≈z
23 ensym ⊢x≈z→z≈x
24 23 ad2antll ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z≈x
25 php3 ⊢y∈Fin∧x⊂y→x≺y
26 13 25 sylan ⊢w∈ω∧y≈w∧x⊂y→x≺y
27 simpllr ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→y≈w
28 sdomentr ⊢x≺y∧y≈w→x≺w
29 26 27 28 syl2an2r ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→x≺w
30 ensdomtr ⊢z≈x∧x≺w→z≺w
31 24 29 30 syl2anc ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z≺w
32 nnon ⊢z∈ω→z∈On
33 32 ad2antrl ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z∈On
34 5 ad3antrrr ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→w∈On
35 sdomel ⊢z∈On∧w∈On→z≺w→z∈w
36 33 34 35 syl2anc ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z≺w→z∈w
37 31 36 mpd ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z∈w
38 37 ex ⊢w∈ω∧y≈w∧x⊂y→z∈ω∧x≈z→z∈w
39 simpr ⊢z∈ω∧x≈z→x≈z
40 38 39 jca2 ⊢w∈ω∧y≈w∧x⊂y→z∈ω∧x≈z→z∈w∧x≈z
41 40 reximdv2 ⊢w∈ω∧y≈w∧x⊂y→∃z∈ωx≈z→∃z∈wx≈z
42 22 41 mpd ⊢w∈ω∧y≈w∧x⊂y→∃z∈wx≈z
43 r19.29 ⊢∀z∈wz∈ω→x≈z→φ∧∃z∈wx≈z→∃z∈wz∈ω→x≈z→φ∧x≈z
44 43 expcom ⊢∃z∈wx≈z→∀z∈wz∈ω→x≈z→φ→∃z∈wz∈ω→x≈z→φ∧x≈z
45 42 44 syl ⊢w∈ω∧y≈w∧x⊂y→∀z∈wz∈ω→x≈z→φ→∃z∈wz∈ω→x≈z→φ∧x≈z
46 ordom ⊢Ord⁡ω
47 ordelss ⊢Ord⁡ω∧w∈ω→w⊆ω
48 46 47 mpan ⊢w∈ω→w⊆ω
49 48 ad2antrr ⊢w∈ω∧y≈w∧x⊂y→w⊆ω
50 49 sseld ⊢w∈ω∧y≈w∧x⊂y→z∈w→z∈ω
51 pm2.27 ⊢z∈ω→z∈ω→x≈z→φ→x≈z→φ
52 51 impd ⊢z∈ω→z∈ω→x≈z→φ∧x≈z→φ
53 50 52 syl6 ⊢w∈ω∧y≈w∧x⊂y→z∈w→z∈ω→x≈z→φ∧x≈z→φ
54 53 rexlimdv ⊢w∈ω∧y≈w∧x⊂y→∃z∈wz∈ω→x≈z→φ∧x≈z→φ
55 45 54 syld ⊢w∈ω∧y≈w∧x⊂y→∀z∈wz∈ω→x≈z→φ→φ
56 55 ex ⊢w∈ω∧y≈w→x⊂y→∀z∈wz∈ω→x≈z→φ→φ
57 56 com23 ⊢w∈ω∧y≈w→∀z∈wz∈ω→x≈z→φ→x⊂y→φ
58 57 alimdv ⊢w∈ω∧y≈w→∀x∀z∈wz∈ω→x≈z→φ→∀xx⊂y→φ
59 17 58 biimtrid ⊢w∈ω∧y≈w→∀z∈wz∈ω→∀xx≈z→φ→∀xx⊂y→φ
60 13 59 3 sylsyld ⊢w∈ω∧y≈w→∀z∈wz∈ω→∀xx≈z→φ→χ
61 60 impancom ⊢w∈ω∧∀z∈wz∈ω→∀xx≈z→φ→y≈w→χ
62 61 alrimiv ⊢w∈ω∧∀z∈wz∈ω→∀xx≈z→φ→∀yy≈w→χ
63 62 expcom ⊢∀z∈wz∈ω→∀xx≈z→φ→w∈ω→∀yy≈w→χ
64 breq1 ⊢x=y→x≈w↔y≈w
65 64 1 imbi12d ⊢x=y→x≈w→φ↔y≈w→χ
66 65 cbvalvw ⊢∀xx≈w→φ↔∀yy≈w→χ
67 63 66 syl6ibr ⊢∀z∈wz∈ω→∀xx≈z→φ→w∈ω→∀xx≈w→φ
68 67 a1i ⊢w∈On→∀z∈wz∈ω→∀xx≈z→φ→w∈ω→∀xx≈w→φ
69 10 68 tfis2 ⊢w∈On→w∈ω→∀xx≈w→φ
70 5 69 mpcom ⊢w∈ω→∀xx≈w→φ
71 70 rgen ⊢∀w∈ω∀xx≈w→φ
72 r19.29 ⊢∀w∈ω∀xx≈w→φ∧∃w∈ωA≈w→∃w∈ω∀xx≈w→φ∧A≈w
73 71 72 mpan ⊢∃w∈ωA≈w→∃w∈ω∀xx≈w→φ∧A≈w
74 4 73 sylbi ⊢A∈Fin→∃w∈ω∀xx≈w→φ∧A≈w
75 breq1 ⊢x=A→x≈w↔A≈w
76 75 2 imbi12d ⊢x=A→x≈w→φ↔A≈w→τ
77 76 spcgv ⊢A∈Fin→∀xx≈w→φ→A≈w→τ
78 77 impd ⊢A∈Fin→∀xx≈w→φ∧A≈w→τ
79 78 rexlimdvw ⊢A∈Fin→∃w∈ω∀xx≈w→φ∧A≈w→τ
80 74 79 mpd ⊢A∈Fin→τ