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

Theorem rankxpsuc 9879
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 9876 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 6280 . . . . . . . 8 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ βˆͺ βˆͺ (𝐴 Γ— 𝐡) = (𝐴 βˆͺ 𝐡))
21fveq2d 6894 . . . . . . 7 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 βˆͺ 𝐡)))
3 rankuni 9860 . . . . . . . 8 (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡))
4 rankuni 9860 . . . . . . . . 9 (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
54unieqi 4920 . . . . . . . 8 βˆͺ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
63, 5eqtri 2758 . . . . . . 7 (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
72, 6eqtr3di 2785 . . . . . 6 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
8 suc11reg 9616 . . . . . 6 (suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
97, 8sylibr 233 . . . . 5 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
109adantl 480 . . . 4 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
11 fvex 6903 . . . . . . . . . . . . . 14 (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ V
12 eleq1 2819 . . . . . . . . . . . . . 14 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ ((rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ V ↔ suc 𝐢 ∈ V))
1311, 12mpbii 232 . . . . . . . . . . . . 13 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ suc 𝐢 ∈ V)
14 sucexb 7794 . . . . . . . . . . . . 13 (𝐢 ∈ V ↔ suc 𝐢 ∈ V)
1513, 14sylibr 233 . . . . . . . . . . . 12 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ 𝐢 ∈ V)
16 nlimsucg 7833 . . . . . . . . . . . 12 (𝐢 ∈ V β†’ Β¬ Lim suc 𝐢)
1715, 16syl 17 . . . . . . . . . . 11 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim suc 𝐢)
18 limeq 6375 . . . . . . . . . . 11 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ (Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) ↔ Lim suc 𝐢))
1917, 18mtbird 324 . . . . . . . . . 10 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
20 rankxplim.1 . . . . . . . . . . 11 𝐴 ∈ V
21 rankxplim.2 . . . . . . . . . . 11 𝐡 ∈ V
2220, 21rankxplim2 9877 . . . . . . . . . 10 (Lim (rankβ€˜(𝐴 Γ— 𝐡)) β†’ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
2319, 22nsyl 140 . . . . . . . . 9 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
2420, 21xpex 7742 . . . . . . . . . . . . . 14 (𝐴 Γ— 𝐡) ∈ V
2524rankeq0 9858 . . . . . . . . . . . . 13 ((𝐴 Γ— 𝐡) = βˆ… ↔ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
2625necon3abii 2985 . . . . . . . . . . . 12 ((𝐴 Γ— 𝐡) β‰  βˆ… ↔ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
27 rankon 9792 . . . . . . . . . . . . . . . 16 (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On
2827onordi 6474 . . . . . . . . . . . . . . 15 Ord (rankβ€˜(𝐴 Γ— 𝐡))
29 ordzsl 7836 . . . . . . . . . . . . . . 15 (Ord (rankβ€˜(𝐴 Γ— 𝐡)) ↔ ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3028, 29mpbi 229 . . . . . . . . . . . . . 14 ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
31 3orass 1088 . . . . . . . . . . . . . 14 (((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))) ↔ ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡)))))
3230, 31mpbi 229 . . . . . . . . . . . . 13 ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3332ori 857 . . . . . . . . . . . 12 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3426, 33sylbi 216 . . . . . . . . . . 11 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
3534ord 860 . . . . . . . . . 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 7833 . . . . . . . . . . . 12 (π‘₯ ∈ V β†’ Β¬ Lim suc π‘₯)
3938elv 3478 . . . . . . . . . . 11 Β¬ Lim suc π‘₯
40 limeq 6375 . . . . . . . . . . 11 ((rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ (Lim (rankβ€˜(𝐴 Γ— 𝐡)) ↔ Lim suc π‘₯))
4139, 40mtbiri 326 . . . . . . . . . 10 ((rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Β¬ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
4241rexlimivw 3149 . . . . . . . . 9 (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Β¬ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
4320, 21rankxplim3 9878 . . . . . . . . 9 (Lim (rankβ€˜(𝐴 Γ— 𝐡)) ↔ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4442, 43sylnib 327 . . . . . . . 8 (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Β¬ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4537, 44syl6com 37 . . . . . . 7 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ Β¬ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
46 unixp0 6281 . . . . . . . . . . . 12 ((𝐴 Γ— 𝐡) = βˆ… ↔ βˆͺ (𝐴 Γ— 𝐡) = βˆ…)
4724uniex 7733 . . . . . . . . . . . . 13 βˆͺ (𝐴 Γ— 𝐡) ∈ V
4847rankeq0 9858 . . . . . . . . . . . 12 (βˆͺ (𝐴 Γ— 𝐡) = βˆ… ↔ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆ…)
494eqeq1i 2735 . . . . . . . . . . . 12 ((rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆ… ↔ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
5046, 48, 493bitri 296 . . . . . . . . . . 11 ((𝐴 Γ— 𝐡) = βˆ… ↔ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
5150necon3abii 2985 . . . . . . . . . 10 ((𝐴 Γ— 𝐡) β‰  βˆ… ↔ Β¬ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
52 onuni 7778 . . . . . . . . . . . . . . 15 ((rankβ€˜(𝐴 Γ— 𝐡)) ∈ On β†’ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On)
5327, 52ax-mp 5 . . . . . . . . . . . . . 14 βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On
5453onordi 6474 . . . . . . . . . . . . 13 Ord βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
55 ordzsl 7836 . . . . . . . . . . . . 13 (Ord βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
5654, 55mpbi 229 . . . . . . . . . . . 12 (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
57 3orass 1088 . . . . . . . . . . . 12 ((βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))) ↔ (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))))
5856, 57mpbi 229 . . . . . . . . . . 11 (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
5958ori 857 . . . . . . . . . 10 (Β¬ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
6051, 59sylbi 216 . . . . . . . . 9 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ ∨ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
6160ord 860 . . . . . . . 8 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (Β¬ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
6261con1d 145 . . . . . . 7 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ (Β¬ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯))
6345, 62syld 47 . . . . . 6 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 β†’ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯))
6463impcom 406 . . . . 5 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯)
65 onsucuni2 7824 . . . . . . 7 ((βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On ∧ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯) β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6653, 65mpan 686 . . . . . 6 (βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6766rexlimivw 3149 . . . . 5 (βˆƒπ‘₯ ∈ On βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6864, 67syl 17 . . . 4 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
6910, 68eqtrd 2770 . . 3 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
70 suc11reg 9616 . . 3 (suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
7169, 70sylibr 233 . 2 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
7237imp 405 . . 3 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯)
73 onsucuni2 7824 . . . . 5 (((rankβ€˜(𝐴 Γ— 𝐡)) ∈ On ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯) β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7427, 73mpan 686 . . . 4 ((rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7574rexlimivw 3149 . . 3 (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc π‘₯ β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7672, 75syl 17 . 2 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7771, 76eqtr2d 2771 1 (((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc 𝐢 ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ (rankβ€˜(𝐴 Γ— 𝐡)) = suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394   ∨ wo 843   ∨ w3o 1084   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆƒwrex 3068  Vcvv 3472   βˆͺ cun 3945  βˆ…c0 4321  βˆͺ cuni 4907   Γ— cxp 5673  Ord word 6362  Oncon0 6363  Lim wlim 6364  suc csuc 6365  β€˜cfv 6542  rankcrnk 9760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-reg 9589  ax-inf2 9638
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-r1 9761  df-rank 9762
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator