ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  findcard2s GIF version

Theorem findcard2s 6686
Description: Variation of findcard2 6685 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)
Hypotheses
Ref Expression
findcard2s.1 (𝑥 = ∅ → (𝜑𝜓))
findcard2s.2 (𝑥 = 𝑦 → (𝜑𝜒))
findcard2s.3 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
findcard2s.4 (𝑥 = 𝐴 → (𝜑𝜏))
findcard2s.5 𝜓
findcard2s.6 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
Assertion
Ref Expression
findcard2s (𝐴 ∈ Fin → 𝜏)
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝜒,𝑥   𝜑,𝑦,𝑧   𝜓,𝑥   𝜏,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)

Proof of Theorem findcard2s
Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard2s.4 . 2 (𝑥 = 𝐴 → (𝜑𝜏))
2 isfi 6558 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 3871 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 230 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1759 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 3871 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 230 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1759 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 3871 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 230 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1759 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 6592 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard2s.5 . . . . . . . . 9 𝜓
14 findcard2s.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 167 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 120 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1390 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 peano3 4439 . . . . . . . . . . . . 13 (𝑣 ∈ ω → suc 𝑣 ≠ ∅)
1918adantr 271 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ≠ ∅)
20 breq1 3870 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
2120anbi2d 453 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
22 peano1 4437 . . . . . . . . . . . . . . . . . 18 ∅ ∈ ω
23 peano2 4438 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
24 nneneq 6653 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2522, 23, 24sylancr 406 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2625biimpa 291 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
2726eqcomd 2100 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
2821, 27syl6bi 162 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
2928com12 30 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
3029necon3d 2306 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
3119, 30mpd 13 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
3231ex 114 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣𝑤 ≠ ∅))
33 nnfi 6668 . . . . . . . . . . . . . . . 16 (suc 𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3423, 33syl 14 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3534adantr 271 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ∈ Fin)
36 enfi 6669 . . . . . . . . . . . . . . 15 (𝑤 ≈ suc 𝑣 → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3736adantl 272 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3835, 37mpbird 166 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ∈ Fin)
39 fin0 6681 . . . . . . . . . . . . 13 (𝑤 ∈ Fin → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
4038, 39syl 14 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
41 simpll 497 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → 𝑣 ∈ ω)
42 dif1en 6675 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
43423expa 1146 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
44 fidifsnid 6667 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ Fin ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
4538, 44sylan 278 . . . . . . . . . . . . . . . 16 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
46 neldifsn 3592 . . . . . . . . . . . . . . . . . 18 ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})
47 vex 2636 . . . . . . . . . . . . . . . . . . . 20 𝑤 ∈ V
48 difexg 4001 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V)
4947, 48ax-mp 7 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∖ {𝑧}) ∈ V
50 breq1 3870 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
5150anbi2d 453 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
52 eleq2 2158 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑧𝑦𝑧 ∈ (𝑤 ∖ {𝑧})))
5352notbid 630 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → (¬ 𝑧𝑦 ↔ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})))
5451, 53anbi12d 458 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧}))))
55 uneq1 3162 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
5655sbceq1d 2859 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑[((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
5756imbi2d 229 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
5854, 57imbi12d 233 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤 ∖ {𝑧}) → ((((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
59 breq1 3870 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
60 findcard2s.2 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝜑𝜒))
6159, 60imbi12d 233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((𝑥𝑣𝜑) ↔ (𝑦𝑣𝜒)))
6261spv 1795 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥(𝑥𝑣𝜑) → (𝑦𝑣𝜒))
63 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑣 → ((𝑦𝑣𝜒) → 𝜒))
6463adantl 272 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜒))
6564adantr 271 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → ((𝑦𝑣𝜒) → 𝜒))
66 rspe 2435 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ∃𝑣 ∈ ω 𝑦𝑣)
67 isfi 6558 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦𝑣)
6866, 67sylibr 133 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → 𝑦 ∈ Fin)
69 findcard2s.6 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
7068, 69sylan 278 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
7165, 70syld 45 . . . . . . . . . . . . . . . . . . . . 21 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → ((𝑦𝑣𝜒) → 𝜃))
7262, 71syl5 32 . . . . . . . . . . . . . . . . . . . 20 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → 𝜃))
73 vex 2636 . . . . . . . . . . . . . . . . . . . . . 22 𝑦 ∈ V
74 vex 2636 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
7574snex 4041 . . . . . . . . . . . . . . . . . . . . . 22 {𝑧} ∈ V
7673, 75unex 4291 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∪ {𝑧}) ∈ V
77 findcard2s.3 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
7876, 77sbcie 2887 . . . . . . . . . . . . . . . . . . . 20 ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑𝜃)
7972, 78syl6ibr 161 . . . . . . . . . . . . . . . . . . 19 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
8049, 58, 79vtocl 2687 . . . . . . . . . . . . . . . . . 18 (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
8146, 80mpan2 417 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
82 dfsbcq 2856 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑[𝑤 / 𝑥]𝜑))
8382imbi2d 229 . . . . . . . . . . . . . . . . 17 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8481, 83syl5ib 153 . . . . . . . . . . . . . . . 16 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8545, 84syl 14 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8641, 43, 85mp2and 425 . . . . . . . . . . . . . 14 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))
8786ex 114 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8887exlimdv 1754 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8940, 88sylbid 149 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
9089ex 114 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
9132, 90mpdd 41 . . . . . . . . 9 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
9291com23 78 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
9392alrimdv 1811 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
94 nfv 1473 . . . . . . . 8 𝑤(𝑥 ≈ suc 𝑣𝜑)
95 nfv 1473 . . . . . . . . 9 𝑥 𝑤 ≈ suc 𝑣
96 nfsbc1v 2872 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
9795, 96nfim 1516 . . . . . . . 8 𝑥(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)
98 breq1 3870 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣𝑤 ≈ suc 𝑣))
99 sbceq1a 2863 . . . . . . . . 9 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
10098, 99imbi12d 233 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
10194, 97, 100cbval 1691 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑))
10293, 101syl6ibr 161 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
1035, 8, 11, 17, 102finds1 4445 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
10410319.21bi 1502 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
105104rexlimiv 2496 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
1062, 105sylbi 120 . 2 (𝑥 ∈ Fin → 𝜑)
1071, 106vtoclga 2699 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wal 1294   = wceq 1296  wex 1433  wcel 1445  wne 2262  wrex 2371  Vcvv 2633  [wsbc 2854  cdif 3010  cun 3011  c0 3302  {csn 3466   class class class wbr 3867  suc csuc 4216  ωcom 4433  cen 6535  Fincfn 6537
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-coll 3975  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-iinf 4431
This theorem depends on definitions:  df-bi 116  df-dc 784  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-if 3414  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-id 4144  df-iord 4217  df-on 4219  df-suc 4222  df-iom 4434  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056  df-fv 5057  df-er 6332  df-en 6538  df-fin 6540
This theorem is referenced by:  findcard2d  6687  findcard2sd  6688  diffifi  6690  ac6sfi  6694  fisseneq  6722  fsum2d  10978  modfsummod  11001  fsumabs  11008  fsumiun  11020
  Copyright terms: Public domain W3C validator