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 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
findcard3OLD.2 ( 𝑥 = 𝐴 → ( 𝜑𝜏 ) )
findcard3OLD.3 ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( 𝑥𝑦𝜑 ) → 𝜒 ) )
Assertion findcard3OLD ( 𝐴 ∈ Fin → 𝜏 )

Proof

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