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

Theorem hashxp 10624
 Description: The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)
Assertion
Ref Expression
hashxp ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))

Proof of Theorem hashxp
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpeq1 4562 . . . 4 (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵))
21fveq2d 5434 . . 3 (𝑥 = ∅ → (♯‘(𝑥 × 𝐵)) = (♯‘(∅ × 𝐵)))
3 fveq2 5430 . . . 4 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
43oveq1d 5798 . . 3 (𝑥 = ∅ → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘∅) · (♯‘𝐵)))
52, 4eqeq12d 2155 . 2 (𝑥 = ∅ → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘(∅ × 𝐵)) = ((♯‘∅) · (♯‘𝐵))))
6 xpeq1 4562 . . . 4 (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵))
76fveq2d 5434 . . 3 (𝑥 = 𝑦 → (♯‘(𝑥 × 𝐵)) = (♯‘(𝑦 × 𝐵)))
8 fveq2 5430 . . . 4 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
98oveq1d 5798 . . 3 (𝑥 = 𝑦 → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘𝑦) · (♯‘𝐵)))
107, 9eqeq12d 2155 . 2 (𝑥 = 𝑦 → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))))
11 xpeq1 4562 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∪ {𝑧}) × 𝐵))
1211fveq2d 5434 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑥 × 𝐵)) = (♯‘((𝑦 ∪ {𝑧}) × 𝐵)))
13 fveq2 5430 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
1413oveq1d 5798 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)))
1512, 14eqeq12d 2155 . 2 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵))))
16 xpeq1 4562 . . . 4 (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵))
1716fveq2d 5434 . . 3 (𝑥 = 𝐴 → (♯‘(𝑥 × 𝐵)) = (♯‘(𝐴 × 𝐵)))
18 fveq2 5430 . . . 4 (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
1918oveq1d 5798 . . 3 (𝑥 = 𝐴 → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))
2017, 19eqeq12d 2155 . 2 (𝑥 = 𝐴 → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵))))
21 0xp 4628 . . . . 5 (∅ × 𝐵) = ∅
2221fveq2i 5433 . . . 4 (♯‘(∅ × 𝐵)) = (♯‘∅)
23 hash0 10595 . . . 4 (♯‘∅) = 0
2422, 23eqtri 2161 . . 3 (♯‘(∅ × 𝐵)) = 0
2523oveq1i 5793 . . . 4 ((♯‘∅) · (♯‘𝐵)) = (0 · (♯‘𝐵))
26 hashcl 10579 . . . . . . 7 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
2726nn0cnd 9076 . . . . . 6 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℂ)
2827mul02d 8198 . . . . 5 (𝐵 ∈ Fin → (0 · (♯‘𝐵)) = 0)
2928adantl 275 . . . 4 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (0 · (♯‘𝐵)) = 0)
3025, 29syl5eq 2185 . . 3 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘∅) · (♯‘𝐵)) = 0)
3124, 30eqtr4id 2192 . 2 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(∅ × 𝐵)) = ((♯‘∅) · (♯‘𝐵)))
32 oveq1 5790 . . . . 5 ((♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵)) → ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵)))
3332adantl 275 . . . 4 (((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵)))
34 xpundir 4605 . . . . . . 7 ((𝑦 ∪ {𝑧}) × 𝐵) = ((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))
3534fveq2i 5433 . . . . . 6 (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵)))
36 simplr 520 . . . . . . . . 9 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → 𝑦 ∈ Fin)
37 simpllr 524 . . . . . . . . 9 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → 𝐵 ∈ Fin)
38 xpfi 6828 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)
3936, 37, 38syl2anc 409 . . . . . . . 8 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (𝑦 × 𝐵) ∈ Fin)
40 vex 2693 . . . . . . . . . . 11 𝑧 ∈ V
41 snfig 6717 . . . . . . . . . . 11 (𝑧 ∈ V → {𝑧} ∈ Fin)
4240, 41ax-mp 5 . . . . . . . . . 10 {𝑧} ∈ Fin
43 xpfi 6828 . . . . . . . . . 10 (({𝑧} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑧} × 𝐵) ∈ Fin)
4442, 43mpan 421 . . . . . . . . 9 (𝐵 ∈ Fin → ({𝑧} × 𝐵) ∈ Fin)
4544ad3antlr 485 . . . . . . . 8 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ({𝑧} × 𝐵) ∈ Fin)
46 simprr 522 . . . . . . . . . 10 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → 𝑧 ∈ (𝐴𝑦))
4746eldifbd 3089 . . . . . . . . 9 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ¬ 𝑧𝑦)
48 inxp 4682 . . . . . . . . . 10 ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ((𝑦 ∩ {𝑧}) × (𝐵𝐵))
49 disjsn 3594 . . . . . . . . . . . . 13 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
5049biimpri 132 . . . . . . . . . . . 12 𝑧𝑦 → (𝑦 ∩ {𝑧}) = ∅)
5150xpeq1d 4571 . . . . . . . . . . 11 𝑧𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵𝐵)) = (∅ × (𝐵𝐵)))
52 0xp 4628 . . . . . . . . . . 11 (∅ × (𝐵𝐵)) = ∅
5351, 52eqtrdi 2189 . . . . . . . . . 10 𝑧𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵𝐵)) = ∅)
5448, 53syl5eq 2185 . . . . . . . . 9 𝑧𝑦 → ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅)
5547, 54syl 14 . . . . . . . 8 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅)
56 hashun 10603 . . . . . . . 8 (((𝑦 × 𝐵) ∈ Fin ∧ ({𝑧} × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵))))
5739, 45, 55, 56syl3anc 1217 . . . . . . 7 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵))))
5840snex 4118 . . . . . . . . . . . 12 {𝑧} ∈ V
5958a1i 9 . . . . . . . . . . 11 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → {𝑧} ∈ V)
60 xpcomeng 6731 . . . . . . . . . . 11 (({𝑧} ∈ V ∧ 𝐵 ∈ Fin) → ({𝑧} × 𝐵) ≈ (𝐵 × {𝑧}))
6159, 37, 60syl2anc 409 . . . . . . . . . 10 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ({𝑧} × 𝐵) ≈ (𝐵 × {𝑧}))
6240a1i 9 . . . . . . . . . . 11 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → 𝑧 ∈ V)
63 xpsneng 6725 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ 𝑧 ∈ V) → (𝐵 × {𝑧}) ≈ 𝐵)
6437, 62, 63syl2anc 409 . . . . . . . . . 10 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (𝐵 × {𝑧}) ≈ 𝐵)
65 entr 6687 . . . . . . . . . 10 ((({𝑧} × 𝐵) ≈ (𝐵 × {𝑧}) ∧ (𝐵 × {𝑧}) ≈ 𝐵) → ({𝑧} × 𝐵) ≈ 𝐵)
6661, 64, 65syl2anc 409 . . . . . . . . 9 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ({𝑧} × 𝐵) ≈ 𝐵)
67 hashen 10582 . . . . . . . . . 10 ((({𝑧} × 𝐵) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘({𝑧} × 𝐵)) = (♯‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵))
6845, 37, 67syl2anc 409 . . . . . . . . 9 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ((♯‘({𝑧} × 𝐵)) = (♯‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵))
6966, 68mpbird 166 . . . . . . . 8 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (♯‘({𝑧} × 𝐵)) = (♯‘𝐵))
7069oveq2d 5799 . . . . . . 7 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)))
7157, 70eqtrd 2173 . . . . . 6 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)))
7235, 71syl5eq 2185 . . . . 5 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)))
7372adantr 274 . . . 4 (((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)))
74 hashunsng 10605 . . . . . . . . 9 (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
7540, 74ax-mp 5 . . . . . . . 8 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
7675oveq1d 5798 . . . . . . 7 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) + 1) · (♯‘𝐵)))
7736, 47, 76syl2anc 409 . . . . . 6 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) + 1) · (♯‘𝐵)))
78 hashcl 10579 . . . . . . . . 9 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
7978nn0cnd 9076 . . . . . . . 8 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℂ)
8036, 79syl 14 . . . . . . 7 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (♯‘𝑦) ∈ ℂ)
8137, 27syl 14 . . . . . . 7 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (♯‘𝐵) ∈ ℂ)
8280, 81adddirp1d 7836 . . . . . 6 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (((♯‘𝑦) + 1) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵)))
8377, 82eqtrd 2173 . . . . 5 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵)))
8483adantr 274 . . . 4 (((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵)))
8533, 73, 843eqtr4d 2183 . . 3 (((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)))
8685ex 114 . 2 ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → ((♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵)) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵))))
87 simpl 108 . 2 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin)
885, 10, 15, 20, 31, 86, 87findcard2sd 6795 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  Vcvv 2690   ∖ cdif 3074   ∪ cun 3075   ∩ cin 3076   ⊆ wss 3077  ∅c0 3369  {csn 3533   class class class wbr 3938   × cxp 4546  ‘cfv 5132  (class class class)co 5783   ≈ cen 6641  Fincfn 6643  ℂcc 7662  0cc0 7664  1c1 7665   + caddc 7667   · cmul 7669  ♯chash 10573 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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461  ax-iinf 4511  ax-cnex 7755  ax-resscn 7756  ax-1cn 7757  ax-1re 7758  ax-icn 7759  ax-addcl 7760  ax-addrcl 7761  ax-mulcl 7762  ax-addcom 7764  ax-mulcom 7765  ax-addass 7766  ax-mulass 7767  ax-distr 7768  ax-i2m1 7769  ax-0lt1 7770  ax-1rid 7771  ax-0id 7772  ax-rnegex 7773  ax-cnre 7775  ax-pre-ltirr 7776  ax-pre-ltwlin 7777  ax-pre-lttrn 7778  ax-pre-apti 7779  ax-pre-ltadd 7780 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4224  df-iord 4297  df-on 4299  df-ilim 4300  df-suc 4302  df-iom 4514  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-riota 5739  df-ov 5786  df-oprab 5787  df-mpo 5788  df-1st 6047  df-2nd 6048  df-recs 6211  df-irdg 6276  df-frec 6297  df-1o 6322  df-oadd 6326  df-er 6438  df-en 6644  df-dom 6645  df-fin 6646  df-pnf 7846  df-mnf 7847  df-xr 7848  df-ltxr 7849  df-le 7850  df-sub 7979  df-neg 7980  df-inn 8765  df-n0 9022  df-z 9099  df-uz 9371  df-fz 9842  df-ihash 10574 This theorem is referenced by:  crth  11956  phimullem  11957
 Copyright terms: Public domain W3C validator