Metamath Proof Explorer

Theorem naddssim

Description: Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024)

Ref Expression
Assertion naddssim Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 oveq2 Could not format ( c = d -> ( A +no c ) = ( A +no d ) ) : No typesetting found for |- ( c = d -> ( A +no c ) = ( A +no d ) ) with typecode |-
2 oveq2 Could not format ( c = d -> ( B +no c ) = ( B +no d ) ) : No typesetting found for |- ( c = d -> ( B +no c ) = ( B +no d ) ) with typecode |-
3 1 2 sseq12d Could not format ( c = d -> ( ( A +no c ) C_ ( B +no c ) <-> ( A +no d ) C_ ( B +no d ) ) ) : No typesetting found for |- ( c = d -> ( ( A +no c ) C_ ( B +no c ) <-> ( A +no d ) C_ ( B +no d ) ) ) with typecode |-
4 3 imbi2d Could not format ( c = d -> ( ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) <-> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) ) : No typesetting found for |- ( c = d -> ( ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) <-> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) ) with typecode |-
5 4 imbi2d Could not format ( c = d -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) ) ) : No typesetting found for |- ( c = d -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) ) ) with typecode |-
6 oveq2 Could not format ( c = C -> ( A +no c ) = ( A +no C ) ) : No typesetting found for |- ( c = C -> ( A +no c ) = ( A +no C ) ) with typecode |-
7 oveq2 Could not format ( c = C -> ( B +no c ) = ( B +no C ) ) : No typesetting found for |- ( c = C -> ( B +no c ) = ( B +no C ) ) with typecode |-
8 6 7 sseq12d Could not format ( c = C -> ( ( A +no c ) C_ ( B +no c ) <-> ( A +no C ) C_ ( B +no C ) ) ) : No typesetting found for |- ( c = C -> ( ( A +no c ) C_ ( B +no c ) <-> ( A +no C ) C_ ( B +no C ) ) ) with typecode |-
9 8 imbi2d Could not format ( c = C -> ( ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) <-> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) : No typesetting found for |- ( c = C -> ( ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) <-> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) with typecode |-
10 9 imbi2d Could not format ( c = C -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) ) : No typesetting found for |- ( c = C -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) ) with typecode |-
11 r19.21v Could not format ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) ) : No typesetting found for |- ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) ) with typecode |-
12 r19.21v Could not format ( A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) <-> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) : No typesetting found for |- ( A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) <-> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) with typecode |-
13 12 imbi2i Could not format ( ( ( A e. On /\ B e. On ) -> A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) -> A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) ) with typecode |-
14 11 13 bitri Could not format ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) ) : No typesetting found for |- ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) ) with typecode |-
15 oveq2 Could not format ( d = w -> ( A +no d ) = ( A +no w ) ) : No typesetting found for |- ( d = w -> ( A +no d ) = ( A +no w ) ) with typecode |-
16 oveq2 Could not format ( d = w -> ( B +no d ) = ( B +no w ) ) : No typesetting found for |- ( d = w -> ( B +no d ) = ( B +no w ) ) with typecode |-
17 15 16 sseq12d Could not format ( d = w -> ( ( A +no d ) C_ ( B +no d ) <-> ( A +no w ) C_ ( B +no w ) ) ) : No typesetting found for |- ( d = w -> ( ( A +no d ) C_ ( B +no d ) <-> ( A +no w ) C_ ( B +no w ) ) ) with typecode |-
18 17 rspccva Could not format ( ( A. d e. c ( A +no d ) C_ ( B +no d ) /\ w e. c ) -> ( A +no w ) C_ ( B +no w ) ) : No typesetting found for |- ( ( A. d e. c ( A +no d ) C_ ( B +no d ) /\ w e. c ) -> ( A +no w ) C_ ( B +no w ) ) with typecode |-
19 18 ad4ant24 Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) C_ ( B +no w ) ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) C_ ( B +no w ) ) with typecode |-
20 simprrl Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. y e. c ( B +no y ) e. x ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. y e. c ( B +no y ) e. x ) with typecode |-
21 oveq2 Could not format ( y = w -> ( B +no y ) = ( B +no w ) ) : No typesetting found for |- ( y = w -> ( B +no y ) = ( B +no w ) ) with typecode |-
22 21 eleq1d Could not format ( y = w -> ( ( B +no y ) e. x <-> ( B +no w ) e. x ) ) : No typesetting found for |- ( y = w -> ( ( B +no y ) e. x <-> ( B +no w ) e. x ) ) with typecode |-
23 22 rspccva Could not format ( ( A. y e. c ( B +no y ) e. x /\ w e. c ) -> ( B +no w ) e. x ) : No typesetting found for |- ( ( A. y e. c ( B +no y ) e. x /\ w e. c ) -> ( B +no w ) e. x ) with typecode |-
24 20 23 sylan Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( B +no w ) e. x ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( B +no w ) e. x ) with typecode |-
25 simplrl ⊢ c ∈ On ∧ A ∈ On ∧ B ∈ On ∧ A ⊆ B → A ∈ On
26 25 adantr Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> A e. On ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> A e. On ) with typecode |-
27 26 adantr Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A e. On ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A e. On ) with typecode |-
28 27 adantr Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> A e. On ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> A e. On ) with typecode |-
29 simp-4l Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> c e. On ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> c e. On ) with typecode |-
30 onelon ⊢ c ∈ On ∧ w ∈ c → w ∈ On
31 29 30 sylan Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> w e. On ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> w e. On ) with typecode |-
32 naddcl Could not format ( ( A e. On /\ w e. On ) -> ( A +no w ) e. On ) : No typesetting found for |- ( ( A e. On /\ w e. On ) -> ( A +no w ) e. On ) with typecode |-
33 28 31 32 syl2anc Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) e. On ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) e. On ) with typecode |-
34 simplrl Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> x e. On ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> x e. On ) with typecode |-
35 ontr2 Could not format ( ( ( A +no w ) e. On /\ x e. On ) -> ( ( ( A +no w ) C_ ( B +no w ) /\ ( B +no w ) e. x ) -> ( A +no w ) e. x ) ) : No typesetting found for |- ( ( ( A +no w ) e. On /\ x e. On ) -> ( ( ( A +no w ) C_ ( B +no w ) /\ ( B +no w ) e. x ) -> ( A +no w ) e. x ) ) with typecode |-
36 33 34 35 syl2anc Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( ( ( A +no w ) C_ ( B +no w ) /\ ( B +no w ) e. x ) -> ( A +no w ) e. x ) ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( ( ( A +no w ) C_ ( B +no w ) /\ ( B +no w ) e. x ) -> ( A +no w ) e. x ) ) with typecode |-
37 19 24 36 mp2and Could not format ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) e. x ) : No typesetting found for |- ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) e. x ) with typecode |-
38 37 ralrimiva Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. w e. c ( A +no w ) e. x ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. w e. c ( A +no w ) e. x ) with typecode |-
39 simpllr Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A C_ B ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A C_ B ) with typecode |-
40 simprrr Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. z e. B ( z +no c ) e. x ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. z e. B ( z +no c ) e. x ) with typecode |-
41 ssralv Could not format ( A C_ B -> ( A. z e. B ( z +no c ) e. x -> A. z e. A ( z +no c ) e. x ) ) : No typesetting found for |- ( A C_ B -> ( A. z e. B ( z +no c ) e. x -> A. z e. A ( z +no c ) e. x ) ) with typecode |-
42 39 40 41 sylc Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. z e. A ( z +no c ) e. x ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. z e. A ( z +no c ) e. x ) with typecode |-
43 38 42 jca Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) ) with typecode |-
44 43 expr Could not format ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ x e. On ) -> ( ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) -> ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) ) ) : No typesetting found for |- ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ x e. On ) -> ( ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) -> ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) ) ) with typecode |-
45 44 ss2rabdv Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } C_ { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } C_ { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } ) with typecode |-
46 intss Could not format ( { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } C_ { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } -> |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } C_ |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) : No typesetting found for |- ( { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } C_ { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } -> |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } C_ |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) with typecode |-
47 45 46 syl Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } C_ |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } C_ |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) with typecode |-
48 simplll Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> c e. On ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> c e. On ) with typecode |-
49 naddov2 Could not format ( ( A e. On /\ c e. On ) -> ( A +no c ) = |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ c e. On ) -> ( A +no c ) = |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } ) with typecode |-
50 26 48 49 syl2anc Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A +no c ) = |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A +no c ) = |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } ) with typecode |-
51 simplrr ⊢ c ∈ On ∧ A ∈ On ∧ B ∈ On ∧ A ⊆ B → B ∈ On
52 51 adantr Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> B e. On ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> B e. On ) with typecode |-
53 naddov2 Could not format ( ( B e. On /\ c e. On ) -> ( B +no c ) = |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) : No typesetting found for |- ( ( B e. On /\ c e. On ) -> ( B +no c ) = |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) with typecode |-
54 52 48 53 syl2anc Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( B +no c ) = |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( B +no c ) = |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } ) with typecode |-
55 47 50 54 3sstr4d Could not format ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A +no c ) C_ ( B +no c ) ) : No typesetting found for |- ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A +no c ) C_ ( B +no c ) ) with typecode |-
56 55 exp31 Could not format ( ( c e. On /\ ( A e. On /\ B e. On ) ) -> ( A C_ B -> ( A. d e. c ( A +no d ) C_ ( B +no d ) -> ( A +no c ) C_ ( B +no c ) ) ) ) : No typesetting found for |- ( ( c e. On /\ ( A e. On /\ B e. On ) ) -> ( A C_ B -> ( A. d e. c ( A +no d ) C_ ( B +no d ) -> ( A +no c ) C_ ( B +no c ) ) ) ) with typecode |-
57 56 a2d Could not format ( ( c e. On /\ ( A e. On /\ B e. On ) ) -> ( ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) : No typesetting found for |- ( ( c e. On /\ ( A e. On /\ B e. On ) ) -> ( ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) with typecode |-
58 57 ex Could not format ( c e. On -> ( ( A e. On /\ B e. On ) -> ( ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) ) : No typesetting found for |- ( c e. On -> ( ( A e. On /\ B e. On ) -> ( ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) ) with typecode |-
59 58 a2d Could not format ( c e. On -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) ) : No typesetting found for |- ( c e. On -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) ) with typecode |-
60 14 59 syl5bi Could not format ( c e. On -> ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) ) : No typesetting found for |- ( c e. On -> ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) ) with typecode |-
61 5 10 60 tfis3 Could not format ( C e. On -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) : No typesetting found for |- ( C e. On -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) with typecode |-
62 61 com12 Could not format ( ( A e. On /\ B e. On ) -> ( C e. On -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( C e. On -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) with typecode |-
63 62 3impia Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) with typecode |-