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

Theorem karden 9892
Description: If we allow the Axiom of Regularity, we can avoid the Axiom of Choice by defining the cardinal number of a set as the set of all sets equinumerous to it and having the least possible rank. This theorem proves the equinumerosity relationship for this definition (compare carden 10548). The hypotheses correspond to the definition of kard of [Enderton] p. 222 (which we don't define separately since currently we do not use it elsewhere). This theorem along with kardex 9891 justify the definition of kard. The restriction to the least rank prevents the proper class that would result from {π‘₯ ∣ π‘₯ β‰ˆ 𝐴}. (Contributed by NM, 18-Dec-2003.) (Revised by AV, 12-Jul-2022.)
Hypotheses
Ref Expression
karden.a 𝐴 ∈ V
karden.c 𝐢 = {π‘₯ ∣ (π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))}
karden.d 𝐷 = {π‘₯ ∣ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))}
Assertion
Ref Expression
karden (𝐢 = 𝐷 ↔ 𝐴 β‰ˆ 𝐡)
Distinct variable groups:   π‘₯,𝑦,𝐴   π‘₯,𝐡,𝑦
Allowed substitution hints:   𝐢(π‘₯,𝑦)   𝐷(π‘₯,𝑦)

Proof of Theorem karden
Dummy variables 𝑧 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 karden.a . . . . . . 7 𝐴 ∈ V
2 breq1 5151 . . . . . . 7 (𝑀 = 𝐴 β†’ (𝑀 β‰ˆ 𝐴 ↔ 𝐴 β‰ˆ 𝐴))
31enref 8983 . . . . . . 7 𝐴 β‰ˆ 𝐴
41, 2, 3ceqsexv2d 3528 . . . . . 6 βˆƒπ‘€ 𝑀 β‰ˆ 𝐴
5 abn0 4380 . . . . . 6 ({𝑀 ∣ 𝑀 β‰ˆ 𝐴} β‰  βˆ… ↔ βˆƒπ‘€ 𝑀 β‰ˆ 𝐴)
64, 5mpbir 230 . . . . 5 {𝑀 ∣ 𝑀 β‰ˆ 𝐴} β‰  βˆ…
7 scott0 9883 . . . . . 6 ({𝑀 ∣ 𝑀 β‰ˆ 𝐴} = βˆ… ↔ {𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} ∣ βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)} = βˆ…)
87necon3bii 2993 . . . . 5 ({𝑀 ∣ 𝑀 β‰ˆ 𝐴} β‰  βˆ… ↔ {𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} ∣ βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)} β‰  βˆ…)
96, 8mpbi 229 . . . 4 {𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} ∣ βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)} β‰  βˆ…
10 rabn0 4385 . . . 4 ({𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} ∣ βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)} β‰  βˆ… ↔ βˆƒπ‘§ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴}βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))
119, 10mpbi 229 . . 3 βˆƒπ‘§ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴}βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)
12 vex 3478 . . . . . . . 8 𝑧 ∈ V
13 breq1 5151 . . . . . . . 8 (𝑀 = 𝑧 β†’ (𝑀 β‰ˆ 𝐴 ↔ 𝑧 β‰ˆ 𝐴))
1412, 13elab 3668 . . . . . . 7 (𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} ↔ 𝑧 β‰ˆ 𝐴)
15 breq1 5151 . . . . . . . 8 (𝑀 = 𝑦 β†’ (𝑀 β‰ˆ 𝐴 ↔ 𝑦 β‰ˆ 𝐴))
1615ralab 3687 . . . . . . 7 (βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦) ↔ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)))
1714, 16anbi12i 627 . . . . . 6 ((𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} ∧ βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)) ↔ (𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))))
18 simpl 483 . . . . . . . . 9 ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) β†’ 𝑧 β‰ˆ 𝐴)
1918a1i 11 . . . . . . . 8 (𝐢 = 𝐷 β†’ ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) β†’ 𝑧 β‰ˆ 𝐴))
20 karden.c . . . . . . . . . . . 12 𝐢 = {π‘₯ ∣ (π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))}
21 karden.d . . . . . . . . . . . 12 𝐷 = {π‘₯ ∣ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))}
2220, 21eqeq12i 2750 . . . . . . . . . . 11 (𝐢 = 𝐷 ↔ {π‘₯ ∣ (π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))} = {π‘₯ ∣ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))})
23 abbib 2804 . . . . . . . . . . 11 ({π‘₯ ∣ (π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))} = {π‘₯ ∣ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))} ↔ βˆ€π‘₯((π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))) ↔ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))))
2422, 23bitri 274 . . . . . . . . . 10 (𝐢 = 𝐷 ↔ βˆ€π‘₯((π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))) ↔ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))))
25 breq1 5151 . . . . . . . . . . . . 13 (π‘₯ = 𝑧 β†’ (π‘₯ β‰ˆ 𝐴 ↔ 𝑧 β‰ˆ 𝐴))
26 fveq2 6891 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑧 β†’ (rankβ€˜π‘₯) = (rankβ€˜π‘§))
2726sseq1d 4013 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑧 β†’ ((rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦) ↔ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)))
2827imbi2d 340 . . . . . . . . . . . . . 14 (π‘₯ = 𝑧 β†’ ((𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)) ↔ (𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))))
2928albidv 1923 . . . . . . . . . . . . 13 (π‘₯ = 𝑧 β†’ (βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)) ↔ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))))
3025, 29anbi12d 631 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ ((π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))) ↔ (𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)))))
31 breq1 5151 . . . . . . . . . . . . 13 (π‘₯ = 𝑧 β†’ (π‘₯ β‰ˆ 𝐡 ↔ 𝑧 β‰ˆ 𝐡))
3227imbi2d 340 . . . . . . . . . . . . . 14 (π‘₯ = 𝑧 β†’ ((𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)) ↔ (𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))))
3332albidv 1923 . . . . . . . . . . . . 13 (π‘₯ = 𝑧 β†’ (βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)) ↔ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))))
3431, 33anbi12d 631 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ ((π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))) ↔ (𝑧 β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)))))
3530, 34bibi12d 345 . . . . . . . . . . 11 (π‘₯ = 𝑧 β†’ (((π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))) ↔ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))) ↔ ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) ↔ (𝑧 β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))))))
3635spvv 2000 . . . . . . . . . 10 (βˆ€π‘₯((π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))) ↔ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))) β†’ ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) ↔ (𝑧 β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)))))
3724, 36sylbi 216 . . . . . . . . 9 (𝐢 = 𝐷 β†’ ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) ↔ (𝑧 β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)))))
38 simpl 483 . . . . . . . . 9 ((𝑧 β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) β†’ 𝑧 β‰ˆ 𝐡)
3937, 38syl6bi 252 . . . . . . . 8 (𝐢 = 𝐷 β†’ ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) β†’ 𝑧 β‰ˆ 𝐡))
4019, 39jcad 513 . . . . . . 7 (𝐢 = 𝐷 β†’ ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) β†’ (𝑧 β‰ˆ 𝐴 ∧ 𝑧 β‰ˆ 𝐡)))
41 ensym 9001 . . . . . . . 8 (𝑧 β‰ˆ 𝐴 β†’ 𝐴 β‰ˆ 𝑧)
42 entr 9004 . . . . . . . 8 ((𝐴 β‰ˆ 𝑧 ∧ 𝑧 β‰ˆ 𝐡) β†’ 𝐴 β‰ˆ 𝐡)
4341, 42sylan 580 . . . . . . 7 ((𝑧 β‰ˆ 𝐴 ∧ 𝑧 β‰ˆ 𝐡) β†’ 𝐴 β‰ˆ 𝐡)
4440, 43syl6 35 . . . . . 6 (𝐢 = 𝐷 β†’ ((𝑧 β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦))) β†’ 𝐴 β‰ˆ 𝐡))
4517, 44biimtrid 241 . . . . 5 (𝐢 = 𝐷 β†’ ((𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} ∧ βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦)) β†’ 𝐴 β‰ˆ 𝐡))
4645expd 416 . . . 4 (𝐢 = 𝐷 β†’ (𝑧 ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} β†’ (βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦) β†’ 𝐴 β‰ˆ 𝐡)))
4746rexlimdv 3153 . . 3 (𝐢 = 𝐷 β†’ (βˆƒπ‘§ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴}βˆ€π‘¦ ∈ {𝑀 ∣ 𝑀 β‰ˆ 𝐴} (rankβ€˜π‘§) βŠ† (rankβ€˜π‘¦) β†’ 𝐴 β‰ˆ 𝐡))
4811, 47mpi 20 . 2 (𝐢 = 𝐷 β†’ 𝐴 β‰ˆ 𝐡)
49 enen2 9120 . . . . 5 (𝐴 β‰ˆ 𝐡 β†’ (π‘₯ β‰ˆ 𝐴 ↔ π‘₯ β‰ˆ 𝐡))
50 enen2 9120 . . . . . . 7 (𝐴 β‰ˆ 𝐡 β†’ (𝑦 β‰ˆ 𝐴 ↔ 𝑦 β‰ˆ 𝐡))
5150imbi1d 341 . . . . . 6 (𝐴 β‰ˆ 𝐡 β†’ ((𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)) ↔ (𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))))
5251albidv 1923 . . . . 5 (𝐴 β‰ˆ 𝐡 β†’ (βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)) ↔ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))))
5349, 52anbi12d 631 . . . 4 (𝐴 β‰ˆ 𝐡 β†’ ((π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦))) ↔ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))))
5453abbidv 2801 . . 3 (𝐴 β‰ˆ 𝐡 β†’ {π‘₯ ∣ (π‘₯ β‰ˆ 𝐴 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐴 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))} = {π‘₯ ∣ (π‘₯ β‰ˆ 𝐡 ∧ βˆ€π‘¦(𝑦 β‰ˆ 𝐡 β†’ (rankβ€˜π‘₯) βŠ† (rankβ€˜π‘¦)))})
5554, 20, 213eqtr4g 2797 . 2 (𝐴 β‰ˆ 𝐡 β†’ 𝐢 = 𝐷)
5648, 55impbii 208 1 (𝐢 = 𝐷 ↔ 𝐴 β‰ˆ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396  βˆ€wal 1539   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βŠ† wss 3948  βˆ…c0 4322   class class class wbr 5148  β€˜cfv 6543   β‰ˆ cen 8938  rankcrnk 9760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-r1 9761  df-rank 9762
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator