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

Theorem fin23lem27 9095
Description: The mapping constructed in fin23lem22 9094 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 7022 . . . 4 Ord ω
2 ordwe 5698 . . . 4 (Ord ω → E We ω)
3 weso 5070 . . . 4 ( E We ω → E Or ω)
41, 2, 3mp2b 10 . . 3 E Or ω
54a1i 11 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6 sopo 5017 . . . . 5 ( E Or ω → E Po ω)
74, 6ax-mp 5 . . . 4 E Po ω
8 poss 5002 . . . 4 (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
97, 8mpi 20 . . 3 (𝑆 ⊆ ω → E Po 𝑆)
109adantr 481 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11 fin23lem22.b . . . 4 𝐶 = (𝑖 ∈ ω ↦ (𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
1211fin23lem22 9094 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto𝑆)
13 f1ofo 6103 . . 3 (𝐶:ω–1-1-onto𝑆𝐶:ω–onto𝑆)
1412, 13syl 17 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto𝑆)
15 nnsdomel 8761 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑎𝑏))
1615adantl 482 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
1716biimpd 219 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
18 fin23lem23 9093 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
1918adantrr 752 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
20 ineq1 3790 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (𝑗𝑆) = (𝑖𝑆))
2120breq1d 4628 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑎 ↔ (𝑖𝑆) ≈ 𝑎))
2221cbvreuv 3166 . . . . . . . . . . . 12 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
2319, 22sylib 208 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
24 nfv 1845 . . . . . . . . . . . 12 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
2521cbvriotav 6577 . . . . . . . . . . . 12 (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
26 ineq1 3790 . . . . . . . . . . . . 13 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆))
2726breq1d 4628 . . . . . . . . . . . 12 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → ((𝑖𝑆) ≈ 𝑎 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2824, 25, 27riotaprop 6590 . . . . . . . . . . 11 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2923, 28syl 17 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
3029simprd 479 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
3130adantrr 752 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32 simprr 795 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎𝑏)
33 fin23lem23 9093 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3433adantrl 751 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3520breq1d 4628 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑏 ↔ (𝑖𝑆) ≈ 𝑏))
3635cbvreuv 3166 . . . . . . . . . . . . . 14 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
3734, 36sylib 208 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
38 nfv 1845 . . . . . . . . . . . . . 14 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
3935cbvriotav 6577 . . . . . . . . . . . . . 14 (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
40 ineq1 3790 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4140breq1d 4628 . . . . . . . . . . . . . 14 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → ((𝑖𝑆) ≈ 𝑏 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4238, 39, 41riotaprop 6590 . . . . . . . . . . . . 13 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4337, 42syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4443simprd 479 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
4544ensymd 7952 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4645adantrr 752 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
47 sdomentr 8039 . . . . . . . . 9 ((𝑎𝑏𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4832, 46, 47syl2anc 692 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
49 ensdomtr 8041 . . . . . . . 8 ((((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5031, 48, 49syl2anc 692 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5150expr 642 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)))
52 simpll 789 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53 omsson 7017 . . . . . . . . 9 ω ⊆ On
5452, 53syl6ss 3600 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
5529simpld 475 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆)
5654, 55sseldd 3589 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On)
5743simpld 475 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆)
5854, 57sseldd 3589 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On)
59 onsdominel 8054 . . . . . . . 8 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
60593expia 1264 . . . . . . 7 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6156, 58, 60syl2anc 692 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6217, 51, 613syld 60 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
63 simprl 793 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
64 breq2 4622 . . . . . . . . 9 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
6564riotabidv 6568 . . . . . . . 8 (𝑖 = 𝑎 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
6665, 11fvmptg 6238 . . . . . . 7 ((𝑎 ∈ ω ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
6763, 55, 66syl2anc 692 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
68 simprr 795 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
69 breq2 4622 . . . . . . . . 9 (𝑖 = 𝑏 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑏))
7069riotabidv 6568 . . . . . . . 8 (𝑖 = 𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7170, 11fvmptg 6238 . . . . . . 7 ((𝑏 ∈ ω ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7268, 57, 71syl2anc 692 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7367, 72eleq12d 2698 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶𝑎) ∈ (𝐶𝑏) ↔ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
7462, 73sylibrd 249 . . . 4 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝐶𝑎) ∈ (𝐶𝑏)))
75 epel 4993 . . . 4 (𝑎 E 𝑏𝑎𝑏)
76 fvex 6160 . . . . 5 (𝐶𝑏) ∈ V
7776epelc 4992 . . . 4 ((𝐶𝑎) E (𝐶𝑏) ↔ (𝐶𝑎) ∈ (𝐶𝑏))
7874, 75, 773imtr4g 285 . . 3 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
7978ralrimivva 2970 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
80 soisoi 6533 . 2 ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
815, 10, 14, 79, 80syl22anc 1324 1 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  wral 2912  ∃!wreu 2914  cin 3559  wss 3560   class class class wbr 4618  cmpt 4678   E cep 4988   Po wpo 4998   Or wor 4999   We wwe 5037  Ord word 5684  Oncon0 5685  ontowfo 5848  1-1-ontowf1o 5849  cfv 5850   Isom wiso 5851  crio 6565  ωcom 7013  cen 7897  csdm 7899  Fincfn 7900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-om 7014  df-wrecs 7353  df-recs 7414  df-1o 7506  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-card 8710
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator