Theorem 5oalem7 27313

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)

Hypotheses

Ref	Expression
5oalem5.1	|- A e. SH
5oalem5.2	|- B e. SH
5oalem5.3	|- C e. SH
5oalem5.4	|- D e. SH
5oalem5.5	|- F e. SH
5oalem5.6	|- G e. SH
5oalem5.7	|- R e. SH
5oalem5.8	|- S e. SH

Assertion

Ref

Expression

5oalem7

|- ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) C_ ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) )

Proof of Theorem 5oalem7

Dummy variables h f g u v w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ee4anv 2080	. . . 4 |- ( E. x E. y E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
2		exrot4 1932	. . . . . 6 |- ( E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. f E. g E. z E. w E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
3		ee4anv 2080	. . . . . . 7 |- ( E. z E. w E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
4	3	2exbii 1719	. . . . . 6 |- ( E. f E. g E. z E. w E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
5	2, 4	bitri 253	. . . . 5 |- ( E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
6	5	2exbii 1719	. . . 4 |- ( E. x E. y E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. x E. y E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
7		elin 3617	. . . . 5 |- ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) <-> ( h e. ( ( A +H B ) i^i ( C +H D ) ) /\ h e. ( ( F +H G ) i^i ( R +H S ) ) ) )
8		5oalem5.1	. . . . . . . . . 10 |- A e. SH
9		5oalem5.2	. . . . . . . . . 10 |- B e. SH
10	8, 9	shseli 26969	. . . . . . . . 9 |- ( h e. ( A +H B ) <-> E. x e. A E. y e. B h = ( x +h y ) )
11		r2ex 2913	. . . . . . . . 9 |- ( E. x e. A E. y e. B h = ( x +h y ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) )
12	10, 11	bitri 253	. . . . . . . 8 |- ( h e. ( A +H B ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) )
13		5oalem5.3	. . . . . . . . . 10 |- C e. SH
14		5oalem5.4	. . . . . . . . . 10 |- D e. SH
15	13, 14	shseli 26969	. . . . . . . . 9 |- ( h e. ( C +H D ) <-> E. z e. C E. w e. D h = ( z +h w ) )
16		r2ex 2913	. . . . . . . . 9 |- ( E. z e. C E. w e. D h = ( z +h w ) <-> E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) )
17	15, 16	bitri 253	. . . . . . . 8 |- ( h e. ( C +H D ) <-> E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) )
18	12, 17	anbi12i 703	. . . . . . 7 |- ( ( h e. ( A +H B ) /\ h e. ( C +H D ) ) <-> ( E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) )
19		elin 3617	. . . . . . 7 |- ( h e. ( ( A +H B ) i^i ( C +H D ) ) <-> ( h e. ( A +H B ) /\ h e. ( C +H D ) ) )
20		ee4anv 2080	. . . . . . 7 |- ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) <-> ( E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) )
21	18, 19, 20	3bitr4ri 282	. . . . . 6 |- ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) <-> h e. ( ( A +H B ) i^i ( C +H D ) ) )
22		5oalem5.5	. . . . . . . . . 10 |- F e. SH
23		5oalem5.6	. . . . . . . . . 10 |- G e. SH
24	22, 23	shseli 26969	. . . . . . . . 9 |- ( h e. ( F +H G ) <-> E. f e. F E. g e. G h = ( f +h g ) )
25		r2ex 2913	. . . . . . . . 9 |- ( E. f e. F E. g e. G h = ( f +h g ) <-> E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) )
26	24, 25	bitri 253	. . . . . . . 8 |- ( h e. ( F +H G ) <-> E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) )
27		5oalem5.7	. . . . . . . . . 10 |- R e. SH
28		5oalem5.8	. . . . . . . . . 10 |- S e. SH
29	27, 28	shseli 26969	. . . . . . . . 9 |- ( h e. ( R +H S ) <-> E. v e. R E. u e. S h = ( v +h u ) )
30		r2ex 2913	. . . . . . . . 9 |- ( E. v e. R E. u e. S h = ( v +h u ) <-> E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) )
31	29, 30	bitri 253	. . . . . . . 8 |- ( h e. ( R +H S ) <-> E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) )
32	26, 31	anbi12i 703	. . . . . . 7 |- ( ( h e. ( F +H G ) /\ h e. ( R +H S ) ) <-> ( E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) )
33		elin 3617	. . . . . . 7 |- ( h e. ( ( F +H G ) i^i ( R +H S ) ) <-> ( h e. ( F +H G ) /\ h e. ( R +H S ) ) )
34		ee4anv 2080	. . . . . . 7 |- ( E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) <-> ( E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) )
35	32, 33, 34	3bitr4ri 282	. . . . . 6 |- ( E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) <-> h e. ( ( F +H G ) i^i ( R +H S ) ) )
36	21, 35	anbi12i 703	. . . . 5 |- ( ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> ( h e. ( ( A +H B ) i^i ( C +H D ) ) /\ h e. ( ( F +H G ) i^i ( R +H S ) ) ) )
37	7, 36	bitr4i 256	. . . 4 |- ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) <-> ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
38	1, 6, 37	3bitr4ri 282	. . 3 |- ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) <-> E. x E. y E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
39	8, 9, 13, 14, 22, 23, 27, 28	5oalem6 27312	. . . . . . 7 |- ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
40	39	exlimivv 1778	. . . . . 6 |- ( E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
41	40	exlimivv 1778	. . . . 5 |- ( E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
42	41	exlimivv 1778	. . . 4 |- ( E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
43	42	exlimivv 1778	. . 3 |- ( E. x E. y E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
44	38, 43	sylbi 199	. 2 |- ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
45	44	ssriv 3436	1 |- ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) C_ ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) )

Syntax hints:   /\ wa 371   = wceq 1444   E.wex 1663   e. wcel 1887   E.wrex 2738   i^i cin 3403   C_ wss 3404  (class class class)co 6290   +h cva 26573   SHcsh 26581   +H cph 26584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-hilex 26652  ax-hfvadd 26653  ax-hvcom 26654  ax-hvass 26655  ax-hv0cl 26656  ax-hvaddid 26657  ax-hfvmul 26658  ax-hvmulid 26659  ax-hvmulass 26660  ax-hvdistr1 26661  ax-hvdistr2 26662  ax-hvmul0 26663

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-er 7363  df-map 7474  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-ltxr 9680  df-sub 9862  df-neg 9863  df-nn 10610  df-grpo 25919  df-ablo 26010  df-hvsub 26624  df-hlim 26625  df-sh 26860  df-ch 26874  df-shs 26961

This theorem is referenced by:  5oai  27314