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

Theorem findcard3 9163
Description: Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Jan-2025.)
Hypotheses
Ref Expression
findcard3.1 (𝑥 = 𝑦 → (𝜑𝜒))
findcard3.2 (𝑥 = 𝐴 → (𝜑𝜏))
findcard3.3 (𝑦 ∈ Fin → (∀𝑥(𝑥𝑦𝜑) → 𝜒))
Assertion
Ref Expression
findcard3 (𝐴 ∈ Fin → 𝜏)
Distinct variable groups:   𝜒,𝑥   𝜏,𝑥   𝑥,𝑦   𝑥,𝐴   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜒(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem findcard3
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 8850 . . 3 (𝐴 ∈ Fin ↔ ∃𝑤 ∈ ω 𝐴𝑤)
2 nnon 7799 . . . . . 6 (𝑤 ∈ ω → 𝑤 ∈ On)
3 eleq1w 2821 . . . . . . . 8 (𝑤 = 𝑧 → (𝑤 ∈ ω ↔ 𝑧 ∈ ω))
4 breq2 5108 . . . . . . . . . 10 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
54imbi1d 342 . . . . . . . . 9 (𝑤 = 𝑧 → ((𝑥𝑤𝜑) ↔ (𝑥𝑧𝜑)))
65albidv 1924 . . . . . . . 8 (𝑤 = 𝑧 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑧𝜑)))
73, 6imbi12d 345 . . . . . . 7 (𝑤 = 𝑧 → ((𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑))))
8 rspe 3231 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ 𝑦𝑤) → ∃𝑤 ∈ ω 𝑦𝑤)
9 isfi 8850 . . . . . . . . . . . . . 14 (𝑦 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑦𝑤)
108, 9sylibr 233 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ 𝑦𝑤) → 𝑦 ∈ Fin)
11 19.21v 1943 . . . . . . . . . . . . . . . 16 (∀𝑥(𝑧 ∈ ω → (𝑥𝑧𝜑)) ↔ (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)))
1211ralbii 3095 . . . . . . . . . . . . . . 15 (∀𝑧𝑤𝑥(𝑧 ∈ ω → (𝑥𝑧𝜑)) ↔ ∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)))
13 ralcom4 3268 . . . . . . . . . . . . . . 15 (∀𝑧𝑤𝑥(𝑧 ∈ ω → (𝑥𝑧𝜑)) ↔ ∀𝑥𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)))
1412, 13bitr3i 277 . . . . . . . . . . . . . 14 (∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)) ↔ ∀𝑥𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)))
15 pssss 4054 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑦𝑥𝑦)
16 ssfi 9051 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ Fin ∧ 𝑥𝑦) → 𝑥 ∈ Fin)
17 isfi 8850 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ Fin ↔ ∃𝑧 ∈ ω 𝑥𝑧)
1816, 17sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ Fin ∧ 𝑥𝑦) → ∃𝑧 ∈ ω 𝑥𝑧)
1910, 15, 18syl2an 597 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → ∃𝑧 ∈ ω 𝑥𝑧)
20 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑧 ∈ ω)
21 nnfi 9045 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ ω → 𝑧 ∈ Fin)
22 ensymfib 9065 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ Fin → (𝑧𝑥𝑥𝑧))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ ω → (𝑧𝑥𝑥𝑧))
2423biimpar 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ω ∧ 𝑥𝑧) → 𝑧𝑥)
2524adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑧𝑥)
26 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑤 ∈ ω)
27 php3 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ Fin ∧ 𝑥𝑦) → 𝑥𝑦)
2810, 27sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → 𝑥𝑦)
2928adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑥𝑦)
30 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑦𝑤)
31 endom 8853 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝑤𝑦𝑤)
32 nnfi 9045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 ∈ ω → 𝑤 ∈ Fin)
33 domfi 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑤 ∈ Fin ∧ 𝑦𝑤) → 𝑦 ∈ Fin)
3432, 33sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑤 ∈ ω ∧ 𝑦𝑤) → 𝑦 ∈ Fin)
35343adant2 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑤 ∈ ω ∧ 𝑥𝑦𝑦𝑤) → 𝑦 ∈ Fin)
36 sdomdom 8854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝑦𝑥𝑦)
37 domfi 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 ∈ Fin ∧ 𝑥𝑦) → 𝑥 ∈ Fin)
3836, 37sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ Fin ∧ 𝑥𝑦) → 𝑥 ∈ Fin)
39383adant3 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ Fin ∧ 𝑥𝑦𝑦𝑤) → 𝑥 ∈ Fin)
4035, 39syld3an1 1411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤 ∈ ω ∧ 𝑥𝑦𝑦𝑤) → 𝑥 ∈ Fin)
41 sdomdomtrfi 9082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ Fin ∧ 𝑥𝑦𝑦𝑤) → 𝑥𝑤)
4240, 41syld3an1 1411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤 ∈ ω ∧ 𝑥𝑦𝑦𝑤) → 𝑥𝑤)
4331, 42syl3an3 1166 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑤 ∈ ω ∧ 𝑥𝑦𝑦𝑤) → 𝑥𝑤)
4426, 29, 30, 43syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑥𝑤)
45 endom 8853 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑥𝑧𝑥)
46 domsdomtrfi 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧 ∈ Fin ∧ 𝑧𝑥𝑥𝑤) → 𝑧𝑤)
4721, 46syl3an1 1164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ω ∧ 𝑧𝑥𝑥𝑤) → 𝑧𝑤)
4845, 47syl3an2 1165 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ ω ∧ 𝑧𝑥𝑥𝑤) → 𝑧𝑤)
4920, 25, 44, 48syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑧𝑤)
50 nnsdomo 9112 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧𝑤𝑧𝑤))
51 nnord 7801 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ ω → Ord 𝑧)
52 nnord 7801 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ ω → Ord 𝑤)
53 ordelpss 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧𝑤𝑧𝑤))
5451, 52, 53syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧𝑤𝑧𝑤))
5550, 54bitr4d 282 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧𝑤𝑧𝑤))
5620, 26, 55syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → (𝑧𝑤𝑧𝑤))
5749, 56mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) ∧ (𝑧 ∈ ω ∧ 𝑥𝑧)) → 𝑧𝑤)
5857ex 414 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → ((𝑧 ∈ ω ∧ 𝑥𝑧) → 𝑧𝑤))
59 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ ω ∧ 𝑥𝑧) → 𝑥𝑧)
6058, 59jca2 515 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → ((𝑧 ∈ ω ∧ 𝑥𝑧) → (𝑧𝑤𝑥𝑧)))
6160reximdv2 3160 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → (∃𝑧 ∈ ω 𝑥𝑧 → ∃𝑧𝑤 𝑥𝑧))
6219, 61mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → ∃𝑧𝑤 𝑥𝑧)
63 r19.29 3116 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)) ∧ ∃𝑧𝑤 𝑥𝑧) → ∃𝑧𝑤 ((𝑧 ∈ ω → (𝑥𝑧𝜑)) ∧ 𝑥𝑧))
6463expcom 415 . . . . . . . . . . . . . . . . . . 19 (∃𝑧𝑤 𝑥𝑧 → (∀𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)) → ∃𝑧𝑤 ((𝑧 ∈ ω → (𝑥𝑧𝜑)) ∧ 𝑥𝑧)))
6562, 64syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → (∀𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)) → ∃𝑧𝑤 ((𝑧 ∈ ω → (𝑥𝑧𝜑)) ∧ 𝑥𝑧)))
66 ordom 7803 . . . . . . . . . . . . . . . . . . . . . . 23 Ord ω
67 ordelss 6330 . . . . . . . . . . . . . . . . . . . . . . 23 ((Ord ω ∧ 𝑤 ∈ ω) → 𝑤 ⊆ ω)
6866, 67mpan 689 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ω → 𝑤 ⊆ ω)
6968ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → 𝑤 ⊆ ω)
7069sseld 3942 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → (𝑧𝑤𝑧 ∈ ω))
71 pm2.27 42 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ω → ((𝑧 ∈ ω → (𝑥𝑧𝜑)) → (𝑥𝑧𝜑)))
7271impd 412 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ω → (((𝑧 ∈ ω → (𝑥𝑧𝜑)) ∧ 𝑥𝑧) → 𝜑))
7370, 72syl6 35 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → (𝑧𝑤 → (((𝑧 ∈ ω → (𝑥𝑧𝜑)) ∧ 𝑥𝑧) → 𝜑)))
7473rexlimdv 3149 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → (∃𝑧𝑤 ((𝑧 ∈ ω → (𝑥𝑧𝜑)) ∧ 𝑥𝑧) → 𝜑))
7565, 74syld 47 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ω ∧ 𝑦𝑤) ∧ 𝑥𝑦) → (∀𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)) → 𝜑))
7675ex 414 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ω ∧ 𝑦𝑤) → (𝑥𝑦 → (∀𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)) → 𝜑)))
7776com23 86 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ω ∧ 𝑦𝑤) → (∀𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)) → (𝑥𝑦𝜑)))
7877alimdv 1920 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ 𝑦𝑤) → (∀𝑥𝑧𝑤 (𝑧 ∈ ω → (𝑥𝑧𝜑)) → ∀𝑥(𝑥𝑦𝜑)))
7914, 78biimtrid 241 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ 𝑦𝑤) → (∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)) → ∀𝑥(𝑥𝑦𝜑)))
80 findcard3.3 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → (∀𝑥(𝑥𝑦𝜑) → 𝜒))
8110, 79, 80sylsyld 61 . . . . . . . . . . . 12 ((𝑤 ∈ ω ∧ 𝑦𝑤) → (∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)) → 𝜒))
8281impancom 453 . . . . . . . . . . 11 ((𝑤 ∈ ω ∧ ∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑))) → (𝑦𝑤𝜒))
8382alrimiv 1931 . . . . . . . . . 10 ((𝑤 ∈ ω ∧ ∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑))) → ∀𝑦(𝑦𝑤𝜒))
8483expcom 415 . . . . . . . . 9 (∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)) → (𝑤 ∈ ω → ∀𝑦(𝑦𝑤𝜒)))
85 breq1 5107 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝑤𝑦𝑤))
86 findcard3.1 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝜑𝜒))
8785, 86imbi12d 345 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥𝑤𝜑) ↔ (𝑦𝑤𝜒)))
8887cbvalvw 2040 . . . . . . . . 9 (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑦(𝑦𝑤𝜒))
8984, 88syl6ibr 252 . . . . . . . 8 (∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑)))
9089a1i 11 . . . . . . 7 (𝑤 ∈ On → (∀𝑧𝑤 (𝑧 ∈ ω → ∀𝑥(𝑥𝑧𝜑)) → (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))))
917, 90tfis2 7784 . . . . . 6 (𝑤 ∈ On → (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑)))
922, 91mpcom 38 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
9392rgen 3065 . . . 4 𝑤 ∈ ω ∀𝑥(𝑥𝑤𝜑)
94 r19.29 3116 . . . 4 ((∀𝑤 ∈ ω ∀𝑥(𝑥𝑤𝜑) ∧ ∃𝑤 ∈ ω 𝐴𝑤) → ∃𝑤 ∈ ω (∀𝑥(𝑥𝑤𝜑) ∧ 𝐴𝑤))
9593, 94mpan 689 . . 3 (∃𝑤 ∈ ω 𝐴𝑤 → ∃𝑤 ∈ ω (∀𝑥(𝑥𝑤𝜑) ∧ 𝐴𝑤))
961, 95sylbi 216 . 2 (𝐴 ∈ Fin → ∃𝑤 ∈ ω (∀𝑥(𝑥𝑤𝜑) ∧ 𝐴𝑤))
97 breq1 5107 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑤𝐴𝑤))
98 findcard3.2 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜏))
9997, 98imbi12d 345 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑤𝜑) ↔ (𝐴𝑤𝜏)))
10099spcgv 3554 . . . 4 (𝐴 ∈ Fin → (∀𝑥(𝑥𝑤𝜑) → (𝐴𝑤𝜏)))
101100impd 412 . . 3 (𝐴 ∈ Fin → ((∀𝑥(𝑥𝑤𝜑) ∧ 𝐴𝑤) → 𝜏))
102101rexlimdvw 3156 . 2 (𝐴 ∈ Fin → (∃𝑤 ∈ ω (∀𝑥(𝑥𝑤𝜑) ∧ 𝐴𝑤) → 𝜏))
10396, 102mpd 15 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wcel 2107  wral 3063  wrex 3072  wss 3909  wpss 3910   class class class wbr 5104  Ord word 6313  Oncon0 6314  ωcom 7793  cen 8814  cdom 8815  csdm 8816  Fincfn 8817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383  ax-un 7663
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-om 7794  df-1o 8380  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821
This theorem is referenced by:  marypha1lem  9303  pgpfac1  19788  pgpfac  19792  fbfinnfr  23114  wilthlem3  26341
  Copyright terms: Public domain W3C validator