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

Theorem fin23lem27 9742
 Description: The mapping constructed in fin23lem22 9741 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 7572 . . . 4 Ord ω
2 ordwe 6173 . . . 4 (Ord ω → E We ω)
3 weso 5511 . . . 4 ( E We ω → E Or ω)
41, 2, 3mp2b 10 . . 3 E Or ω
54a1i 11 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6 sopo 5457 . . . . 5 ( E Or ω → E Po ω)
74, 6ax-mp 5 . . . 4 E Po ω
8 poss 5441 . . . 4 (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
97, 8mpi 20 . . 3 (𝑆 ⊆ ω → E Po 𝑆)
109adantr 484 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11 fin23lem22.b . . . 4 𝐶 = (𝑖 ∈ ω ↦ (𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
1211fin23lem22 9741 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto𝑆)
13 f1ofo 6598 . . 3 (𝐶:ω–1-1-onto𝑆𝐶:ω–onto𝑆)
1412, 13syl 17 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto𝑆)
15 nnsdomel 9406 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑎𝑏))
1615adantl 485 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
1716biimpd 232 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
18 fin23lem23 9740 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
1918adantrr 716 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
20 ineq1 4131 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (𝑗𝑆) = (𝑖𝑆))
2120breq1d 5041 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑎 ↔ (𝑖𝑆) ≈ 𝑎))
2221cbvreuvw 3398 . . . . . . . . . . . 12 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
2319, 22sylib 221 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
24 nfv 1915 . . . . . . . . . . . 12 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
2521cbvriotavw 7104 . . . . . . . . . . . 12 (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
26 ineq1 4131 . . . . . . . . . . . . 13 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆))
2726breq1d 5041 . . . . . . . . . . . 12 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → ((𝑖𝑆) ≈ 𝑎 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2824, 25, 27riotaprop 7121 . . . . . . . . . . 11 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2923, 28syl 17 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
3029simprd 499 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
3130adantrr 716 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32 simprr 772 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎𝑏)
33 fin23lem23 9740 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3433adantrl 715 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3520breq1d 5041 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑏 ↔ (𝑖𝑆) ≈ 𝑏))
3635cbvreuvw 3398 . . . . . . . . . . . . . 14 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
3734, 36sylib 221 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
38 nfv 1915 . . . . . . . . . . . . . 14 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
3935cbvriotavw 7104 . . . . . . . . . . . . . 14 (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
40 ineq1 4131 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4140breq1d 5041 . . . . . . . . . . . . . 14 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → ((𝑖𝑆) ≈ 𝑏 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4238, 39, 41riotaprop 7121 . . . . . . . . . . . . 13 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4337, 42syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4443simprd 499 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
4544ensymd 8546 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4645adantrr 716 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
47 sdomentr 8638 . . . . . . . . 9 ((𝑎𝑏𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4832, 46, 47syl2anc 587 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
49 ensdomtr 8640 . . . . . . . 8 ((((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5031, 48, 49syl2anc 587 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5150expr 460 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)))
52 simpll 766 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53 omsson 7567 . . . . . . . . 9 ω ⊆ On
5452, 53sstrdi 3927 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
5529simpld 498 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆)
5654, 55sseldd 3916 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On)
5743simpld 498 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆)
5854, 57sseldd 3916 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On)
59 onsdominel 8653 . . . . . . . 8 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
60593expia 1118 . . . . . . 7 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6156, 58, 60syl2anc 587 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6217, 51, 613syld 60 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
63 breq2 5035 . . . . . . . 8 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
6463riotabidv 7096 . . . . . . 7 (𝑖 = 𝑎 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
65 simprl 770 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
6611, 64, 65, 55fvmptd3 6769 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
67 breq2 5035 . . . . . . . 8 (𝑖 = 𝑏 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑏))
6867riotabidv 7096 . . . . . . 7 (𝑖 = 𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
69 simprr 772 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
7011, 68, 69, 57fvmptd3 6769 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7166, 70eleq12d 2884 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶𝑎) ∈ (𝐶𝑏) ↔ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
7262, 71sylibrd 262 . . . 4 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝐶𝑎) ∈ (𝐶𝑏)))
73 epel 5434 . . . 4 (𝑎 E 𝑏𝑎𝑏)
74 fvex 6659 . . . . 5 (𝐶𝑏) ∈ V
7574epeli 5433 . . . 4 ((𝐶𝑎) E (𝐶𝑏) ↔ (𝐶𝑎) ∈ (𝐶𝑏))
7672, 73, 753imtr4g 299 . . 3 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
7776ralrimivva 3156 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
78 soisoi 7061 . 2 ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
795, 10, 14, 77, 78syl22anc 837 1 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃!wreu 3108   ∩ cin 3880   ⊆ wss 3881   class class class wbr 5031   ↦ cmpt 5111   E cep 5430   Po wpo 5437   Or wor 5438   We wwe 5478  Ord word 6159  Oncon0 6160  –onto→wfo 6323  –1-1-onto→wf1o 6324  ‘cfv 6325   Isom wiso 6326  ℩crio 7093  ωcom 7563   ≈ cen 8492   ≺ csdm 8494  Fincfn 8495 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-om 7564  df-wrecs 7933  df-recs 7994  df-1o 8088  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-card 9355 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator