MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  findcard2OLD Structured version   Visualization version   GIF version

Theorem findcard2OLD 9302
Description: Obsolete version of findcard2 9182 as of 6-Aug-2024. (Contributed by Jeff Madsen, 8-Jul-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
findcard2OLD.1 (𝑥 = ∅ → (𝜑𝜓))
findcard2OLD.2 (𝑥 = 𝑦 → (𝜑𝜒))
findcard2OLD.3 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
findcard2OLD.4 (𝑥 = 𝐴 → (𝜑𝜏))
findcard2OLD.5 𝜓
findcard2OLD.6 (𝑦 ∈ Fin → (𝜒𝜃))
Assertion
Ref Expression
findcard2OLD (𝐴 ∈ Fin → 𝜏)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)

Proof of Theorem findcard2OLD
Dummy variables 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard2OLD.4 . 2 (𝑥 = 𝐴 → (𝜑𝜏))
2 isfi 8990 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 5148 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 340 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1915 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 5148 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 340 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1915 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 5148 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 340 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1915 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 9031 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard2OLD.5 . . . . . . . . 9 𝜓
14 findcard2OLD.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 257 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 216 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1789 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 nsuceq0 6448 . . . . . . . . . . . 12 suc 𝑣 ≠ ∅
19 breq1 5147 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
2019anbi2d 628 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
21 peano1 7889 . . . . . . . . . . . . . . . . . 18 ∅ ∈ ω
22 peano2 7891 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
23 nneneq 9227 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2421, 22, 23sylancr 585 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2524biimpa 475 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
2625eqcomd 2731 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
2720, 26biimtrdi 252 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
2827com12 32 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
2928necon3d 2951 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
3018, 29mpi 20 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
3130ex 411 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣𝑤 ≠ ∅))
32 n0 4343 . . . . . . . . . . . 12 (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤)
33 dif1enOLD 9180 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
34333expia 1118 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (𝑤 ∖ {𝑧}) ≈ 𝑣))
35 snssi 4808 . . . . . . . . . . . . . . . . . 18 (𝑧𝑤 → {𝑧} ⊆ 𝑤)
36 uncom 4147 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝑤 ∖ {𝑧}))
37 undif 4478 . . . . . . . . . . . . . . . . . . . 20 ({𝑧} ⊆ 𝑤 ↔ ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
3837biimpi 215 . . . . . . . . . . . . . . . . . . 19 ({𝑧} ⊆ 𝑤 → ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
3936, 38eqtrid 2777 . . . . . . . . . . . . . . . . . 18 ({𝑧} ⊆ 𝑤 → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
40 vex 3467 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
4140difexi 5326 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∖ {𝑧}) ∈ V
42 breq1 5147 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
4342anbi2d 628 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
44 uneq1 4150 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
4544sbceq1d 3775 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑[((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
4645imbi2d 339 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
4743, 46imbi12d 343 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
48 breq1 5147 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
49 findcard2OLD.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝜑𝜒))
5048, 49imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝑥𝑣𝜑) ↔ (𝑦𝑣𝜒)))
5150spvv 1992 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥(𝑥𝑣𝜑) → (𝑦𝑣𝜒))
52 rspe 3237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ∃𝑣 ∈ ω 𝑦𝑣)
53 isfi 8990 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦𝑣)
5452, 53sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → 𝑦 ∈ Fin)
55 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑣 → ((𝑦𝑣𝜒) → 𝜒))
5655adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜒))
57 findcard2OLD.6 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ Fin → (𝜒𝜃))
5854, 56, 57sylsyld 61 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜃))
5951, 58syl5 34 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → 𝜃))
60 vex 3467 . . . . . . . . . . . . . . . . . . . . . . 23 𝑦 ∈ V
61 snex 5428 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑧} ∈ V
6260, 61unex 7743 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∪ {𝑧}) ∈ V
63 findcard2OLD.3 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
6462, 63sbcie 3814 . . . . . . . . . . . . . . . . . . . . 21 ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑𝜃)
6559, 64imbitrrdi 251 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ ω ∧ 𝑦𝑣) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
6641, 47, 65vtocl 3537 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
67 dfsbcq 3772 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑[𝑤 / 𝑥]𝜑))
6867imbi2d 339 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
6966, 68imbitrid 243 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7035, 39, 693syl 18 . . . . . . . . . . . . . . . . 17 (𝑧𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7170expd 414 . . . . . . . . . . . . . . . 16 (𝑧𝑤 → (𝑣 ∈ ω → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7271com12 32 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → (𝑧𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7372adantr 479 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7434, 73mpdd 43 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7574exlimdv 1928 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7632, 75biimtrid 241 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7776ex 411 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
7831, 77mpdd 43 . . . . . . . . 9 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
7978com23 86 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
8079alrimdv 1924 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
81 nfv 1909 . . . . . . . 8 𝑤(𝑥 ≈ suc 𝑣𝜑)
82 nfv 1909 . . . . . . . . 9 𝑥 𝑤 ≈ suc 𝑣
83 nfsbc1v 3790 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
8482, 83nfim 1891 . . . . . . . 8 𝑥(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)
85 breq1 5147 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣𝑤 ≈ suc 𝑣))
86 sbceq1a 3781 . . . . . . . . 9 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
8785, 86imbi12d 343 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
8881, 84, 87cbvalv1 2331 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑))
8980, 88imbitrrdi 251 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
905, 8, 11, 17, 89finds1 7901 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
919019.21bi 2177 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
9291rexlimiv 3138 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
932, 92sylbi 216 . 2 (𝑥 ∈ Fin → 𝜑)
941, 93vtoclga 3557 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1531   = wceq 1533  wex 1773  wcel 2098  wne 2930  wrex 3060  [wsbc 3770  cdif 3938  cun 3939  wss 3941  c0 4319  {csn 4625   class class class wbr 5144  suc csuc 6367  ωcom 7865  cen 8954  Fincfn 8957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5295  ax-nul 5302  ax-pr 5424  ax-un 7735
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7866  df-1o 8480  df-en 8958  df-fin 8961
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator