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

Theorem fin23lem27 9188
Description: The mapping constructed in fin23lem22 9187 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 7116 . . . 4 Ord ω
2 ordwe 5774 . . . 4 (Ord ω → E We ω)
3 weso 5134 . . . 4 ( E We ω → E Or ω)
41, 2, 3mp2b 10 . . 3 E Or ω
54a1i 11 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6 sopo 5081 . . . . 5 ( E Or ω → E Po ω)
74, 6ax-mp 5 . . . 4 E Po ω
8 poss 5066 . . . 4 (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
97, 8mpi 20 . . 3 (𝑆 ⊆ ω → E Po 𝑆)
109adantr 480 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11 fin23lem22.b . . . 4 𝐶 = (𝑖 ∈ ω ↦ (𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
1211fin23lem22 9187 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto𝑆)
13 f1ofo 6182 . . 3 (𝐶:ω–1-1-onto𝑆𝐶:ω–onto𝑆)
1412, 13syl 17 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto𝑆)
15 nnsdomel 8854 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑎𝑏))
1615adantl 481 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
1716biimpd 219 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏𝑎𝑏))
18 fin23lem23 9186 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
1918adantrr 753 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎)
20 ineq1 3840 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (𝑗𝑆) = (𝑖𝑆))
2120breq1d 4695 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑎 ↔ (𝑖𝑆) ≈ 𝑎))
2221cbvreuv 3203 . . . . . . . . . . . 12 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑎 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
2319, 22sylib 208 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
24 nfv 1883 . . . . . . . . . . . 12 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
2521cbvriotav 6662 . . . . . . . . . . . 12 (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑎)
26 ineq1 3840 . . . . . . . . . . . . 13 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆))
2726breq1d 4695 . . . . . . . . . . . 12 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) → ((𝑖𝑆) ≈ 𝑎 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2824, 25, 27riotaprop 6675 . . . . . . . . . . 11 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑎 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
2923, 28syl 17 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
3029simprd 478 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
3130adantrr 753 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32 simprr 811 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎𝑏)
33 fin23lem23 9186 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3433adantrl 752 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏)
3520breq1d 4695 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑗𝑆) ≈ 𝑏 ↔ (𝑖𝑆) ≈ 𝑏))
3635cbvreuv 3203 . . . . . . . . . . . . . 14 (∃!𝑗𝑆 (𝑗𝑆) ≈ 𝑏 ↔ ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
3734, 36sylib 208 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
38 nfv 1883 . . . . . . . . . . . . . 14 𝑖((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
3935cbvriotav 6662 . . . . . . . . . . . . . 14 (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) = (𝑖𝑆 (𝑖𝑆) ≈ 𝑏)
40 ineq1 3840 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → (𝑖𝑆) = ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4140breq1d 4695 . . . . . . . . . . . . . 14 (𝑖 = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) → ((𝑖𝑆) ≈ 𝑏 ↔ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4238, 39, 41riotaprop 6675 . . . . . . . . . . . . 13 (∃!𝑖𝑆 (𝑖𝑆) ≈ 𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4337, 42syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
4443simprd 478 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
4544ensymd 8048 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4645adantrr 753 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
47 sdomentr 8135 . . . . . . . . 9 ((𝑎𝑏𝑏 ≈ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
4832, 46, 47syl2anc 694 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → 𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
49 ensdomtr 8137 . . . . . . . 8 ((((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎𝑎 ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5031, 48, 49syl2anc 694 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎𝑏)) → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆))
5150expr 642 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)))
52 simpll 805 . . . . . . . . 9 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53 omsson 7111 . . . . . . . . 9 ω ⊆ On
5452, 53syl6ss 3648 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
5529simpld 474 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆)
5654, 55sseldd 3637 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On)
5743simpld 474 . . . . . . . 8 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆)
5854, 57sseldd 3637 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On)
59 onsdominel 8150 . . . . . . . 8 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On ∧ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆)) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
60593expia 1286 . . . . . . 7 (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ On ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ On) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6156, 58, 60syl2anc 694 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∩ 𝑆) → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
6217, 51, 613syld 60 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
63 simprl 809 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
64 breq2 4689 . . . . . . . . 9 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
6564riotabidv 6653 . . . . . . . 8 (𝑖 = 𝑎 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
6665, 11fvmptg 6319 . . . . . . 7 ((𝑎 ∈ ω ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ 𝑆) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
6763, 55, 66syl2anc 694 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑎) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
68 simprr 811 . . . . . . 7 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
69 breq2 4689 . . . . . . . . 9 (𝑖 = 𝑏 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑏))
7069riotabidv 6653 . . . . . . . 8 (𝑖 = 𝑏 → (𝑗𝑆 (𝑗𝑆) ≈ 𝑖) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7170, 11fvmptg 6319 . . . . . . 7 ((𝑏 ∈ ω ∧ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏) ∈ 𝑆) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7268, 57, 71syl2anc 694 . . . . . 6 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶𝑏) = (𝑗𝑆 (𝑗𝑆) ≈ 𝑏))
7367, 72eleq12d 2724 . . . . 5 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶𝑎) ∈ (𝐶𝑏) ↔ (𝑗𝑆 (𝑗𝑆) ≈ 𝑎) ∈ (𝑗𝑆 (𝑗𝑆) ≈ 𝑏)))
7462, 73sylibrd 249 . . . 4 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎𝑏 → (𝐶𝑎) ∈ (𝐶𝑏)))
75 epel 5061 . . . 4 (𝑎 E 𝑏𝑎𝑏)
76 fvex 6239 . . . . 5 (𝐶𝑏) ∈ V
7776epelc 5060 . . . 4 ((𝐶𝑎) E (𝐶𝑏) ↔ (𝐶𝑎) ∈ (𝐶𝑏))
7874, 75, 773imtr4g 285 . . 3 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
7978ralrimivva 3000 . 2 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))
80 soisoi 6618 . 2 ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶𝑎) E (𝐶𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
815, 10, 14, 79, 80syl22anc 1367 1 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  ∃!wreu 2943  cin 3606  wss 3607   class class class wbr 4685  cmpt 4762   E cep 5057   Po wpo 5062   Or wor 5063   We wwe 5101  Ord word 5760  Oncon0 5761  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926   Isom wiso 5927  crio 6650  ωcom 7107  cen 7994  csdm 7996  Fincfn 7997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-om 7108  df-wrecs 7452  df-recs 7513  df-1o 7605  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator