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

Theorem findcard2s 6880
Description: Variation of findcard2 6879 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 6751 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 4002 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 231 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1822 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 4002 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 231 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1822 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 4002 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 231 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1822 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 6785 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard2s.5 . . . . . . . . 9 𝜓
14 findcard2s.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 168 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 121 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1447 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 peano3 4589 . . . . . . . . . . . . 13 (𝑣 ∈ ω → suc 𝑣 ≠ ∅)
1918adantr 276 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ≠ ∅)
20 breq1 4001 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
2120anbi2d 464 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
22 peano1 4587 . . . . . . . . . . . . . . . . . 18 ∅ ∈ ω
23 peano2 4588 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
24 nneneq 6847 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2522, 23, 24sylancr 414 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2625biimpa 296 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
2726eqcomd 2181 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
2821, 27syl6bi 163 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
2928com12 30 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
3029necon3d 2389 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
3119, 30mpd 13 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
3231ex 115 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣𝑤 ≠ ∅))
33 nnfi 6862 . . . . . . . . . . . . . . . 16 (suc 𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3423, 33syl 14 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3534adantr 276 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ∈ Fin)
36 enfi 6863 . . . . . . . . . . . . . . 15 (𝑤 ≈ suc 𝑣 → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3736adantl 277 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3835, 37mpbird 167 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ∈ Fin)
39 fin0 6875 . . . . . . . . . . . . 13 (𝑤 ∈ Fin → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
4038, 39syl 14 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
41 simpll 527 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → 𝑣 ∈ ω)
42 dif1en 6869 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
43423expa 1203 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
44 fidifsnid 6861 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ Fin ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
4538, 44sylan 283 . . . . . . . . . . . . . . . 16 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
46 neldifsn 3719 . . . . . . . . . . . . . . . . . 18 ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})
47 vex 2738 . . . . . . . . . . . . . . . . . . . 20 𝑤 ∈ V
48 difexg 4139 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V)
4947, 48ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∖ {𝑧}) ∈ V
50 breq1 4001 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
5150anbi2d 464 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
52 eleq2 2239 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑧𝑦𝑧 ∈ (𝑤 ∖ {𝑧})))
5352notbid 667 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → (¬ 𝑧𝑦 ↔ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})))
5451, 53anbi12d 473 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧}))))
55 uneq1 3280 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
5655sbceq1d 2965 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑[((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
5756imbi2d 230 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
5854, 57imbi12d 234 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤 ∖ {𝑧}) → ((((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
59 breq1 4001 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
60 findcard2s.2 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝜑𝜒))
6159, 60imbi12d 234 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((𝑥𝑣𝜑) ↔ (𝑦𝑣𝜒)))
6261spv 1858 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥(𝑥𝑣𝜑) → (𝑦𝑣𝜒))
63 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑣 → ((𝑦𝑣𝜒) → 𝜒))
6463adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜒))
6564adantr 276 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → ((𝑦𝑣𝜒) → 𝜒))
66 rspe 2524 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ∃𝑣 ∈ ω 𝑦𝑣)
67 isfi 6751 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦𝑣)
6866, 67sylibr 134 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → 𝑦 ∈ Fin)
69 findcard2s.6 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
7068, 69sylan 283 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
7165, 70syld 45 . . . . . . . . . . . . . . . . . . . . 21 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → ((𝑦𝑣𝜒) → 𝜃))
7262, 71syl5 32 . . . . . . . . . . . . . . . . . . . 20 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → 𝜃))
73 vex 2738 . . . . . . . . . . . . . . . . . . . . . 22 𝑦 ∈ V
74 vex 2738 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
7574snex 4180 . . . . . . . . . . . . . . . . . . . . . 22 {𝑧} ∈ V
7673, 75unex 4435 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∪ {𝑧}) ∈ V
77 findcard2s.3 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
7876, 77sbcie 2995 . . . . . . . . . . . . . . . . . . . 20 ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑𝜃)
7972, 78syl6ibr 162 . . . . . . . . . . . . . . . . . . 19 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
8049, 58, 79vtocl 2789 . . . . . . . . . . . . . . . . . 18 (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
8146, 80mpan2 425 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
82 dfsbcq 2962 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑[𝑤 / 𝑥]𝜑))
8382imbi2d 230 . . . . . . . . . . . . . . . . 17 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8481, 83syl5ib 154 . . . . . . . . . . . . . . . 16 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8545, 84syl 14 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8641, 43, 85mp2and 433 . . . . . . . . . . . . . 14 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))
8786ex 115 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8887exlimdv 1817 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8940, 88sylbid 150 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
9089ex 115 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
9132, 90mpdd 41 . . . . . . . . 9 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
9291com23 78 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
9392alrimdv 1874 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
94 nfv 1526 . . . . . . . 8 𝑤(𝑥 ≈ suc 𝑣𝜑)
95 nfv 1526 . . . . . . . . 9 𝑥 𝑤 ≈ suc 𝑣
96 nfsbc1v 2979 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
9795, 96nfim 1570 . . . . . . . 8 𝑥(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)
98 breq1 4001 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣𝑤 ≈ suc 𝑣))
99 sbceq1a 2970 . . . . . . . . 9 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
10098, 99imbi12d 234 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
10194, 97, 100cbval 1752 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑))
10293, 101syl6ibr 162 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
1035, 8, 11, 17, 102finds1 4595 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
10410319.21bi 1556 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
105104rexlimiv 2586 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
1062, 105sylbi 121 . 2 (𝑥 ∈ Fin → 𝜑)
1071, 106vtoclga 2801 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wal 1351   = wceq 1353  wex 1490  wcel 2146  wne 2345  wrex 2454  Vcvv 2735  [wsbc 2960  cdif 3124  cun 3125  c0 3420  {csn 3589   class class class wbr 3998  suc csuc 4359  ωcom 4583  cen 6728  Fincfn 6730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-if 3533  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-iord 4360  df-on 4362  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-er 6525  df-en 6731  df-fin 6733
This theorem is referenced by:  findcard2d  6881  findcard2sd  6882  diffifi  6884  ac6sfi  6888  fisseneq  6921  fsum2d  11409  modfsummod  11432  fsumabs  11439  fsumiun  11451  fprod2d  11597
  Copyright terms: Public domain W3C validator