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

Theorem fin23lem27 9373
Description: The mapping constructed in fin23lem22 9372 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 7242 . . . 4 Ord ω
2 ordwe 5890 . . . 4 (Ord ω → E We ω)
3 weso 5254 . . . 4 ( E We ω → E Or ω)
41, 2, 3mp2b 10 . . 3 E Or ω
54a1i 11 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6 sopo 5201 . . . . 5 ( E Or ω → E Po ω)
74, 6ax-mp 5 . . . 4 E Po ω
8 poss 5186 . . . 4 (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
97, 8mpi 20 . . 3 (𝑆 ⊆ ω → E Po 𝑆)
109adantr 467 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11 fin23lem22.b . . . 4 𝐶 = (𝑖 ∈ ω ↦ (𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
1211fin23lem22 9372 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto𝑆)
13 f1ofo 6300 . . 3 (𝐶:ω–1-1-onto𝑆𝐶:ω–onto𝑆)
1412, 13syl 17 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto𝑆)
15 nnsdomel 9037 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑎𝑏))
1615adantl 468 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
1716biimpd 220 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
18 fin23lem23 9371 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
1918adantrr 697 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
20 ineq1 3965 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (𝑗𝑆) = (𝑖𝑆))
2120breq1d 4807 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑎 ↔ (𝑖𝑆) ≈ 𝑎))
2221cbvreuv 3326 . . . . . . . . . . . 12 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
2319, 22sylib 209 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
24 nfv 1998 . . . . . . . . . . . 12 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
2521cbvriotav 6784 . . . . . . . . . . . 12 (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
26 ineq1 3965 . . . . . . . . . . . . 13 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆))
2726breq1d 4807 . . . . . . . . . . . 12 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → ((𝑖𝑆) ≈ 𝑎 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2824, 25, 27riotaprop 6797 . . . . . . . . . . 11 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2923, 28syl 17 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
3029simprd 484 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
3130adantrr 697 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32 simprr 778 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎𝑏)
33 fin23lem23 9371 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3433adantrl 696 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3520breq1d 4807 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑏 ↔ (𝑖𝑆) ≈ 𝑏))
3635cbvreuv 3326 . . . . . . . . . . . . . 14 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
3734, 36sylib 209 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
38 nfv 1998 . . . . . . . . . . . . . 14 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
3935cbvriotav 6784 . . . . . . . . . . . . . 14 (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
40 ineq1 3965 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4140breq1d 4807 . . . . . . . . . . . . . 14 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → ((𝑖𝑆) ≈ 𝑏 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4238, 39, 41riotaprop 6797 . . . . . . . . . . . . 13 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4337, 42syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4443simprd 484 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
4544ensymd 8181 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4645adantrr 697 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
47 sdomentr 8271 . . . . . . . . 9 ((𝑎𝑏𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4832, 46, 47syl2anc 574 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
49 ensdomtr 8273 . . . . . . . 8 ((((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5031, 48, 49syl2anc 574 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5150expr 445 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)))
52 simpll 772 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53 omsson 7237 . . . . . . . . 9 ω ⊆ On
5452, 53syl6ss 3770 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
5529simpld 483 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆)
5654, 55sseldd 3759 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On)
5743simpld 483 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆)
5854, 57sseldd 3759 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On)
59 onsdominel 8286 . . . . . . . 8 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
60593expia 1141 . . . . . . 7 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6156, 58, 60syl2anc 574 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6217, 51, 613syld 60 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
63 simprl 776 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
64 breq2 4801 . . . . . . . . 9 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
6564riotabidv 6775 . . . . . . . 8 (𝑖 = 𝑎 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
6665, 11fvmptg 6439 . . . . . . 7 ((𝑎 ∈ ω ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
6763, 55, 66syl2anc 574 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
68 simprr 778 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
69 breq2 4801 . . . . . . . . 9 (𝑖 = 𝑏 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑏))
7069riotabidv 6775 . . . . . . . 8 (𝑖 = 𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7170, 11fvmptg 6439 . . . . . . 7 ((𝑏 ∈ ω ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7268, 57, 71syl2anc 574 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7367, 72eleq12d 2847 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶𝑎) ∈ (𝐶𝑏) ↔ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
7462, 73sylibrd 250 . . . 4 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝐶𝑎) ∈ (𝐶𝑏)))
75 epel 5179 . . . 4 (𝑎 E 𝑏𝑎𝑏)
76 fvex 6359 . . . . 5 (𝐶𝑏) ∈ V
7776epelc 5178 . . . 4 ((𝐶𝑎) E (𝐶𝑏) ↔ (𝐶𝑎) ∈ (𝐶𝑏))
7874, 75, 773imtr4g 286 . . 3 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
7978ralrimivva 3123 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
80 soisoi 6740 . 2 ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
815, 10, 14, 79, 80syl22anc 856 1 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383   = wceq 1634  wcel 2148  wral 3064  ∃!wreu 3066  cin 3728  wss 3729   class class class wbr 4797  cmpt 4876   E cep 5175   Po wpo 5182   Or wor 5183   We wwe 5221  Ord word 5876  Oncon0 5877  ontowfo 6040  1-1-ontowf1o 6041  cfv 6042   Isom wiso 6043  crio 6772  ωcom 7233  cen 8127  csdm 8129  Fincfn 8130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-om 7234  df-wrecs 7580  df-recs 7642  df-1o 7734  df-er 7917  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-card 8986
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator