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

Theorem fin23lem27 10366
Description: The mapping constructed in fin23lem22 10365 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014.)
Hypothesis
Ref Expression
fin23lem22.b 𝐶 = (𝑖 ∈ ω ↦ (𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
Assertion
Ref Expression
fin23lem27 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))
Distinct variable group:   𝑖,𝑗,𝑆
Allowed substitution hints:   𝐶(𝑖,𝑗)

Proof of Theorem fin23lem27
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordom 7897 . . . 4 Ord ω
2 ordwe 6399 . . . 4 (Ord ω → E We ω)
3 weso 5680 . . . 4 ( E We ω → E Or ω)
41, 2, 3mp2b 10 . . 3 E Or ω
54a1i 11 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6 sopo 5616 . . . . 5 ( E Or ω → E Po ω)
74, 6ax-mp 5 . . . 4 E Po ω
8 poss 5599 . . . 4 (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
97, 8mpi 20 . . 3 (𝑆 ⊆ ω → E Po 𝑆)
109adantr 480 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11 fin23lem22.b . . . 4 𝐶 = (𝑖 ∈ ω ↦ (𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
1211fin23lem22 10365 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto𝑆)
13 f1ofo 6856 . . 3 (𝐶:ω–1-1-onto𝑆𝐶:ω–onto𝑆)
1412, 13syl 17 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto𝑆)
15 nnsdomel 10028 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑎𝑏))
1615adantl 481 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
1716biimpd 229 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
18 fin23lem23 10364 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
1918adantrr 717 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
20 ineq1 4221 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (𝑗𝑆) = (𝑖𝑆))
2120breq1d 5158 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑎 ↔ (𝑖𝑆) ≈ 𝑎))
2221cbvreuvw 3402 . . . . . . . . . . . 12 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
2319, 22sylib 218 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
24 nfv 1912 . . . . . . . . . . . 12 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
2521cbvriotavw 7398 . . . . . . . . . . . 12 (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
26 ineq1 4221 . . . . . . . . . . . . 13 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆))
2726breq1d 5158 . . . . . . . . . . . 12 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → ((𝑖𝑆) ≈ 𝑎 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2824, 25, 27riotaprop 7415 . . . . . . . . . . 11 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2923, 28syl 17 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
3029simprd 495 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
3130adantrr 717 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32 simprr 773 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎𝑏)
33 fin23lem23 10364 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3433adantrl 716 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3520breq1d 5158 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑏 ↔ (𝑖𝑆) ≈ 𝑏))
3635cbvreuvw 3402 . . . . . . . . . . . . . 14 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
3734, 36sylib 218 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
38 nfv 1912 . . . . . . . . . . . . . 14 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
3935cbvriotavw 7398 . . . . . . . . . . . . . 14 (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
40 ineq1 4221 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4140breq1d 5158 . . . . . . . . . . . . . 14 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → ((𝑖𝑆) ≈ 𝑏 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4238, 39, 41riotaprop 7415 . . . . . . . . . . . . 13 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4337, 42syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4443simprd 495 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
4544ensymd 9044 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4645adantrr 717 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
47 sdomentr 9150 . . . . . . . . 9 ((𝑎𝑏𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4832, 46, 47syl2anc 584 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
49 ensdomtr 9152 . . . . . . . 8 ((((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5031, 48, 49syl2anc 584 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5150expr 456 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)))
52 simpll 767 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53 omsson 7891 . . . . . . . . 9 ω ⊆ On
5452, 53sstrdi 4008 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
5529simpld 494 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆)
5654, 55sseldd 3996 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On)
5743simpld 494 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆)
5854, 57sseldd 3996 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On)
59 onsdominel 9165 . . . . . . . 8 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
60593expia 1120 . . . . . . 7 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6156, 58, 60syl2anc 584 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6217, 51, 613syld 60 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
63 breq2 5152 . . . . . . . 8 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
6463riotabidv 7390 . . . . . . 7 (𝑖 = 𝑎 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
65 simprl 771 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
6611, 64, 65, 55fvmptd3 7039 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
67 breq2 5152 . . . . . . . 8 (𝑖 = 𝑏 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑏))
6867riotabidv 7390 . . . . . . 7 (𝑖 = 𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
69 simprr 773 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
7011, 68, 69, 57fvmptd3 7039 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7166, 70eleq12d 2833 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶𝑎) ∈ (𝐶𝑏) ↔ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
7262, 71sylibrd 259 . . . 4 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝐶𝑎) ∈ (𝐶𝑏)))
73 epel 5592 . . . 4 (𝑎 E 𝑏𝑎𝑏)
74 fvex 6920 . . . . 5 (𝐶𝑏) ∈ V
7574epeli 5591 . . . 4 ((𝐶𝑎) E (𝐶𝑏) ↔ (𝐶𝑎) ∈ (𝐶𝑏))
7672, 73, 753imtr4g 296 . . 3 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
7776ralrimivva 3200 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
78 soisoi 7348 . 2 ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
795, 10, 14, 77, 78syl22anc 839 1 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  ∃!wreu 3376  cin 3962  wss 3963   class class class wbr 5148  cmpt 5231   E cep 5588   Po wpo 5595   Or wor 5596   We wwe 5640  Ord word 6385  Oncon0 6386  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563   Isom wiso 6564  crio 7387  ωcom 7887  cen 8981  csdm 8983  Fincfn 8984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-1o 8505  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-card 9977
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator