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

Theorem findcard2s 6784
 Description: Variation of findcard2 6783 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 6655 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 3933 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 230 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1796 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 3933 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 230 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1796 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 3933 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 230 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1796 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 6689 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard2s.5 . . . . . . . . 9 𝜓
14 findcard2s.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 167 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 120 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1425 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 peano3 4510 . . . . . . . . . . . . 13 (𝑣 ∈ ω → suc 𝑣 ≠ ∅)
1918adantr 274 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ≠ ∅)
20 breq1 3932 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
2120anbi2d 459 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
22 peano1 4508 . . . . . . . . . . . . . . . . . 18 ∅ ∈ ω
23 peano2 4509 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
24 nneneq 6751 . . . . . . . . . . . . . . . . . 18 ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2522, 23, 24sylancr 410 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
2625biimpa 294 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
2726eqcomd 2145 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
2821, 27syl6bi 162 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
2928com12 30 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
3029necon3d 2352 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
3119, 30mpd 13 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
3231ex 114 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣𝑤 ≠ ∅))
33 nnfi 6766 . . . . . . . . . . . . . . . 16 (suc 𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3423, 33syl 14 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → suc 𝑣 ∈ Fin)
3534adantr 274 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ∈ Fin)
36 enfi 6767 . . . . . . . . . . . . . . 15 (𝑤 ≈ suc 𝑣 → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3736adantl 275 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
3835, 37mpbird 166 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ∈ Fin)
39 fin0 6779 . . . . . . . . . . . . 13 (𝑤 ∈ Fin → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
4038, 39syl 14 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧𝑤))
41 simpll 518 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → 𝑣 ∈ ω)
42 dif1en 6773 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
43423expa 1181 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
44 fidifsnid 6765 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ Fin ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
4538, 44sylan 281 . . . . . . . . . . . . . . . 16 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
46 neldifsn 3653 . . . . . . . . . . . . . . . . . 18 ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})
47 vex 2689 . . . . . . . . . . . . . . . . . . . 20 𝑤 ∈ V
48 difexg 4069 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V)
4947, 48ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∖ {𝑧}) ∈ V
50 breq1 3932 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
5150anbi2d 459 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
52 eleq2 2203 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑧𝑦𝑧 ∈ (𝑤 ∖ {𝑧})))
5352notbid 656 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → (¬ 𝑧𝑦 ↔ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})))
5451, 53anbi12d 464 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧}))))
55 uneq1 3223 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
5655sbceq1d 2914 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑[((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
5756imbi2d 229 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
5854, 57imbi12d 233 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤 ∖ {𝑧}) → ((((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
59 breq1 3932 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
60 findcard2s.2 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝜑𝜒))
6159, 60imbi12d 233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((𝑥𝑣𝜑) ↔ (𝑦𝑣𝜒)))
6261spv 1832 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥(𝑥𝑣𝜑) → (𝑦𝑣𝜒))
63 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑣 → ((𝑦𝑣𝜒) → 𝜒))
6463adantl 275 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ((𝑦𝑣𝜒) → 𝜒))
6564adantr 274 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → ((𝑦𝑣𝜒) → 𝜒))
66 rspe 2481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ω ∧ 𝑦𝑣) → ∃𝑣 ∈ ω 𝑦𝑣)
67 isfi 6655 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦𝑣)
6866, 67sylibr 133 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ω ∧ 𝑦𝑣) → 𝑦 ∈ Fin)
69 findcard2s.6 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
7068, 69sylan 281 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
7165, 70syld 45 . . . . . . . . . . . . . . . . . . . . 21 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → ((𝑦𝑣𝜒) → 𝜃))
7262, 71syl5 32 . . . . . . . . . . . . . . . . . . . 20 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → 𝜃))
73 vex 2689 . . . . . . . . . . . . . . . . . . . . . 22 𝑦 ∈ V
74 vex 2689 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
7574snex 4109 . . . . . . . . . . . . . . . . . . . . . 22 {𝑧} ∈ V
7673, 75unex 4362 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∪ {𝑧}) ∈ V
77 findcard2s.3 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
7876, 77sbcie 2943 . . . . . . . . . . . . . . . . . . . 20 ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑𝜃)
7972, 78syl6ibr 161 . . . . . . . . . . . . . . . . . . 19 (((𝑣 ∈ ω ∧ 𝑦𝑣) ∧ ¬ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
8049, 58, 79vtocl 2740 . . . . . . . . . . . . . . . . . 18 (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
8146, 80mpan2 421 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
82 dfsbcq 2911 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑[𝑤 / 𝑥]𝜑))
8382imbi2d 229 . . . . . . . . . . . . . . . . 17 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥𝑣𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8481, 83syl5ib 153 . . . . . . . . . . . . . . . 16 (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8545, 84syl 14 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8641, 43, 85mp2and 429 . . . . . . . . . . . . . 14 (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧𝑤) → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))
8786ex 114 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8887exlimdv 1791 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧𝑤 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
8940, 88sylbid 149 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
9089ex 114 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑))))
9132, 90mpdd 41 . . . . . . . . 9 (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥𝑣𝜑) → [𝑤 / 𝑥]𝜑)))
9291com23 78 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
9392alrimdv 1848 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
94 nfv 1508 . . . . . . . 8 𝑤(𝑥 ≈ suc 𝑣𝜑)
95 nfv 1508 . . . . . . . . 9 𝑥 𝑤 ≈ suc 𝑣
96 nfsbc1v 2927 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
9795, 96nfim 1551 . . . . . . . 8 𝑥(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)
98 breq1 3932 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣𝑤 ≈ suc 𝑣))
99 sbceq1a 2918 . . . . . . . . 9 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
10098, 99imbi12d 233 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑)))
10194, 97, 100cbval 1727 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣[𝑤 / 𝑥]𝜑))
10293, 101syl6ibr 161 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
1035, 8, 11, 17, 102finds1 4516 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
10410319.21bi 1537 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
105104rexlimiv 2543 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
1062, 105sylbi 120 . 2 (𝑥 ∈ Fin → 𝜑)
1071, 106vtoclga 2752 1 (𝐴 ∈ Fin → 𝜏)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1329   = wceq 1331  ∃wex 1468   ∈ wcel 1480   ≠ wne 2308  ∃wrex 2417  Vcvv 2686  [wsbc 2909   ∖ cdif 3068   ∪ cun 3069  ∅c0 3363  {csn 3527   class class class wbr 3929  suc csuc 4287  ωcom 4504   ≈ cen 6632  Fincfn 6634 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-er 6429  df-en 6635  df-fin 6637 This theorem is referenced by:  findcard2d  6785  findcard2sd  6786  diffifi  6788  ac6sfi  6792  fisseneq  6820  fsum2d  11211  modfsummod  11234  fsumabs  11241  fsumiun  11253
 Copyright terms: Public domain W3C validator