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

Theorem rankxpsuc 9877
Description: The rank of a Cartesian product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxplim 9874 for the limit ordinal case. (Contributed by NM, 19-Sep-2006.)
Hypotheses
Ref Expression
rankxplim.1 𝐴 ∈ V
rankxplim.2 𝐡 ∈ V
Assertion
Ref Expression
rankxpsuc (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ (rankβ€˜(𝐴 Γ— 𝐡)) = suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)))

Proof of Theorem rankxpsuc
Dummy variable π‘₯ is distinct from all other variables.
StepHypRef Expression
1 unixp 6282 . . . . . . . 8 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ βˆͺ βˆͺ (𝐴 Γ— 𝐡) = (𝐴 βˆͺ 𝐡))
21fveq2d 6896 . . . . . . 7 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 βˆͺ 𝐡)))
3 rankuni 9858 . . . . . . . 8 (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡))
4 rankuni 9858 . . . . . . . . 9 (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
54unieqi 4922 . . . . . . . 8 βˆͺ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
63, 5eqtri 2761 . . . . . . 7 (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
72, 6eqtr3di 2788 . . . . . 6 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
8 suc11reg 9614 . . . . . 6 (suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
97, 8sylibr 233 . . . . 5 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
109adantl 483 . . . 4 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
11 fvex 6905 . . . . . . . . . . . . . 14 (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ V
12 eleq1 2822 . . . . . . . . . . . . . 14 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ ((rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ V ↔ suc 𝐢 ∈ V))
1311, 12mpbii 232 . . . . . . . . . . . . 13 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ suc 𝐢 ∈ V)
14 sucexb 7792 . . . . . . . . . . . . 13 (𝐢 ∈ V ↔ suc 𝐢 ∈ V)
1513, 14sylibr 233 . . . . . . . . . . . 12 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ 𝐢 ∈ V)
16 nlimsucg 7831 . . . . . . . . . . . 12 (𝐢 ∈ V β†’ Β¬ Lim suc 𝐢)
1715, 16syl 17 . . . . . . . . . . 11 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim suc 𝐢)
18 limeq 6377 . . . . . . . . . . 11 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ (Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) ↔ Lim suc 𝐢))
1917, 18mtbird 325 . . . . . . . . . 10 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
20 rankxplim.1 . . . . . . . . . . 11 𝐴 ∈ V
21 rankxplim.2 . . . . . . . . . . 11 𝐡 ∈ V
2220, 21rankxplim2 9875 . . . . . . . . . 10 (Lim (rankβ€˜(𝐴 Γ— 𝐡)) β†’ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
2319, 22nsyl 140 . . . . . . . . 9 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
2420, 21xpex 7740 . . . . . . . . . . . . . 14 (𝐴 Γ— 𝐡) ∈ V
2524rankeq0 9856 . . . . . . . . . . . . 13 ((𝐴 Γ— 𝐡) = βˆ… ↔ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
2625necon3abii 2988 . . . . . . . . . . . 12 ((𝐴 Γ— 𝐡) β‰  βˆ… ↔ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
27 rankon 9790 . . . . . . . . . . . . . . . 16 (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On
2827onordi 6476 . . . . . . . . . . . . . . 15 Ord (rankβ€˜(𝐴 Γ— 𝐡))
29 ordzsl 7834 . . . . . . . . . . . . . . 15 (Ord (rankβ€˜(𝐴 Γ— 𝐡)) ↔ ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3028, 29mpbi 229 . . . . . . . . . . . . . 14 ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
31 3orass 1091 . . . . . . . . . . . . . 14 (((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))) ↔ ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡)))))
3230, 31mpbi 229 . . . . . . . . . . . . 13 ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3332ori 860 . . . . . . . . . . . 12 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3426, 33sylbi 216 . . . . . . . . . . 11 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3534ord 863 . . . . . . . . . 10 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (Β¬ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3635con1d 145 . . . . . . . . 9 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (Β¬ Lim (rankβ€˜(𝐴 Γ— 𝐡)) β†’ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯))
3723, 36syl5com 31 . . . . . . . 8 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯))
38 nlimsucg 7831 . . . . . . . . . . . 12 (π‘₯ ∈ V β†’ Β¬ Lim suc π‘₯)
3938elv 3481 . . . . . . . . . . 11 Β¬ Lim suc π‘₯
40 limeq 6377 . . . . . . . . . . 11 ((rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ (Lim (rankβ€˜(𝐴 Γ— 𝐡)) ↔ Lim suc π‘₯))
4139, 40mtbiri 327 . . . . . . . . . 10 ((rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Β¬ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
4241rexlimivw 3152 . . . . . . . . 9 (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Β¬ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
4320, 21rankxplim3 9876 . . . . . . . . 9 (Lim (rankβ€˜(𝐴 Γ— 𝐡)) ↔ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4442, 43sylnib 328 . . . . . . . 8 (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Β¬ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4537, 44syl6com 37 . . . . . . 7 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
46 unixp0 6283 . . . . . . . . . . . 12 ((𝐴 Γ— 𝐡) = βˆ… ↔ βˆͺ (𝐴 Γ— 𝐡) = βˆ…)
4724uniex 7731 . . . . . . . . . . . . 13 βˆͺ (𝐴 Γ— 𝐡) ∈ V
4847rankeq0 9856 . . . . . . . . . . . 12 (βˆͺ (𝐴 Γ— 𝐡) = βˆ… ↔ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆ…)
494eqeq1i 2738 . . . . . . . . . . . 12 ((rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆ… ↔ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
5046, 48, 493bitri 297 . . . . . . . . . . 11 ((𝐴 Γ— 𝐡) = βˆ… ↔ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
5150necon3abii 2988 . . . . . . . . . 10 ((𝐴 Γ— 𝐡) β‰  βˆ… ↔ Β¬ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
52 onuni 7776 . . . . . . . . . . . . . . 15 ((rankβ€˜(𝐴 Γ— 𝐡)) ∈ On β†’ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On)
5327, 52ax-mp 5 . . . . . . . . . . . . . 14 βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On
5453onordi 6476 . . . . . . . . . . . . 13 Ord βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
55 ordzsl 7834 . . . . . . . . . . . . 13 (Ord βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
5654, 55mpbi 229 . . . . . . . . . . . 12 (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
57 3orass 1091 . . . . . . . . . . . 12 ((βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))) ↔ (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))))
5856, 57mpbi 229 . . . . . . . . . . 11 (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
5958ori 860 . . . . . . . . . 10 (Β¬ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
6051, 59sylbi 216 . . . . . . . . 9 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
6160ord 863 . . . . . . . 8 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (Β¬ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
6261con1d 145 . . . . . . 7 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (Β¬ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯))
6345, 62syld 47 . . . . . 6 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯))
6463impcom 409 . . . . 5 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯)
65 onsucuni2 7822 . . . . . . 7 ((βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On ∧ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯) β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6653, 65mpan 689 . . . . . 6 (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6766rexlimivw 3152 . . . . 5 (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6864, 67syl 17 . . . 4 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6910, 68eqtrd 2773 . . 3 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
70 suc11reg 9614 . . 3 (suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
7169, 70sylibr 233 . 2 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
7237imp 408 . . 3 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯)
73 onsucuni2 7822 . . . . 5 (((rankβ€˜(𝐴 Γ— 𝐡)) ∈ On ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯) β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7427, 73mpan 689 . . . 4 ((rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7574rexlimivw 3152 . . 3 (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7672, 75syl 17 . 2 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7771, 76eqtr2d 2774 1 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ (rankβ€˜(𝐴 Γ— 𝐡)) = suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∨ wo 846   ∨ w3o 1087   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆƒwrex 3071  Vcvv 3475   βˆͺ cun 3947  βˆ…c0 4323  βˆͺ cuni 4909   Γ— cxp 5675  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367  β€˜cfv 6544  rankcrnk 9758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-reg 9587  ax-inf2 9636
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-r1 9759  df-rank 9760
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator