Metamath Proof Explorer

Theorem naddasslem1

Description: Lemma for naddass . Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion naddasslem1 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } )

Proof

Step Hyp Ref Expression
1 naddcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On )
2 1 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no B ) e. On )
3 simp3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> C e. On )
4 naddov3 
 |-  ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { a e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ a } )
5 4 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no B ) = |^| { a e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ a } )
6 intmin 
 |-  ( C e. On -> |^| { c e. On | C C_ c } = C )
7 6 eqcomd 
 |-  ( C e. On -> C = |^| { c e. On | C C_ c } )
8 7 3ad2ant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> C = |^| { c e. On | C C_ c } )
9 2 3 5 8 naddunif 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } )
10 df-3an 
 |-  ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) )
11 unss 
 |-  ( ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x ) <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) C_ x )
12 ancom 
 |-  ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x ) )
13 xpundir 
 |-  ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) = ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) )
14 13 imaeq2i 
 |-  ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) = ( +no " ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) )
15 imaundi 
 |-  ( +no " ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) = ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) )
16 14 15 eqtri 
 |-  ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) = ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) )
17 16 sseq1i 
 |-  ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) C_ x )
18 11 12 17 3bitr4i 
 |-  ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) <-> ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x )
19 18 anbi1i 
 |-  ( ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) )
20 unss 
 |-  ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x )
21 10 19 20 3bitrri 
 |-  ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x <-> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) )
22 naddfn 
 |-  +no Fn ( On X. On )
23 fnfun 
 |-  ( +no Fn ( On X. On ) -> Fun +no )
24 22 23 ax-mp 
 |-  Fun +no
25 imassrn 
 |-  ( +no " ( A X. { B } ) ) C_ ran +no
26 naddf 
 |-  +no : ( On X. On ) --> On
27 frn 
 |-  ( +no : ( On X. On ) --> On -> ran +no C_ On )
28 26 27 ax-mp 
 |-  ran +no C_ On
29 25 28 sstri 
 |-  ( +no " ( A X. { B } ) ) C_ On
30 simpl3 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> C e. On )
31 30 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { C } C_ On )
32 xpss12 
 |-  ( ( ( +no " ( A X. { B } ) ) C_ On /\ { C } C_ On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ ( On X. On ) )
33 29 31 32 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ ( On X. On ) )
34 22 fndmi 
 |-  dom +no = ( On X. On )
35 33 34 sseqtrrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ dom +no )
36 funimassov 
 |-  ( ( Fun +no /\ ( ( +no " ( A X. { B } ) ) X. { C } ) C_ dom +no ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x ) )
37 24 35 36 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x ) )
38 oveq2 
 |-  ( c = C -> ( p +no c ) = ( p +no C ) )
39 38 eleq1d 
 |-  ( c = C -> ( ( p +no c ) e. x <-> ( p +no C ) e. x ) )
40 39 ralsng 
 |-  ( C e. On -> ( A. c e. { C } ( p +no c ) e. x <-> ( p +no C ) e. x ) )
41 30 40 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. c e. { C } ( p +no c ) e. x <-> ( p +no C ) e. x ) )
42 41 ralbidv 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x <-> A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x ) )
43 onss 
 |-  ( A e. On -> A C_ On )
44 43 3ad2ant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> A C_ On )
45 44 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> A C_ On )
46 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> B e. On )
47 46 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { B } C_ On )
48 xpss12 
 |-  ( ( A C_ On /\ { B } C_ On ) -> ( A X. { B } ) C_ ( On X. On ) )
49 45 47 48 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A X. { B } ) C_ ( On X. On ) )
50 oveq1 
 |-  ( p = ( a +no b ) -> ( p +no C ) = ( ( a +no b ) +no C ) )
51 50 eleq1d 
 |-  ( p = ( a +no b ) -> ( ( p +no C ) e. x <-> ( ( a +no b ) +no C ) e. x ) )
52 51 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x ) )
53 22 49 52 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x ) )
54 oveq2 
 |-  ( b = B -> ( a +no b ) = ( a +no B ) )
55 54 oveq1d 
 |-  ( b = B -> ( ( a +no b ) +no C ) = ( ( a +no B ) +no C ) )
56 55 eleq1d 
 |-  ( b = B -> ( ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) )
57 56 ralsng 
 |-  ( B e. On -> ( A. b e. { B } ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) )
58 46 57 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. b e. { B } ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) )
59 58 ralbidv 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) )
60 53 59 bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) )
61 37 42 60 3bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) )
62 imassrn 
 |-  ( +no " ( { A } X. B ) ) C_ ran +no
63 62 28 sstri 
 |-  ( +no " ( { A } X. B ) ) C_ On
64 xpss12 
 |-  ( ( ( +no " ( { A } X. B ) ) C_ On /\ { C } C_ On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ ( On X. On ) )
65 63 31 64 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ ( On X. On ) )
66 65 34 sseqtrrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ dom +no )
67 funimassov 
 |-  ( ( Fun +no /\ ( ( +no " ( { A } X. B ) ) X. { C } ) C_ dom +no ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x ) )
68 24 66 67 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x ) )
69 41 ralbidv 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x <-> A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x ) )
70 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> A e. On )
71 70 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { A } C_ On )
72 onss 
 |-  ( B e. On -> B C_ On )
73 72 3ad2ant2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> B C_ On )
74 73 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> B C_ On )
75 xpss12 
 |-  ( ( { A } C_ On /\ B C_ On ) -> ( { A } X. B ) C_ ( On X. On ) )
76 71 74 75 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { A } X. B ) C_ ( On X. On ) )
77 51 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x ) )
78 22 76 77 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x ) )
79 oveq1 
 |-  ( a = A -> ( a +no b ) = ( A +no b ) )
80 79 oveq1d 
 |-  ( a = A -> ( ( a +no b ) +no C ) = ( ( A +no b ) +no C ) )
81 80 eleq1d 
 |-  ( a = A -> ( ( ( a +no b ) +no C ) e. x <-> ( ( A +no b ) +no C ) e. x ) )
82 81 ralbidv 
 |-  ( a = A -> ( A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) )
83 82 ralsng 
 |-  ( A e. On -> ( A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) )
84 70 83 syl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) )
85 78 84 bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) )
86 68 69 85 3bitrd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) )
87 2 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A +no B ) e. On )
88 87 snssd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { ( A +no B ) } C_ On )
89 onss 
 |-  ( C e. On -> C C_ On )
90 89 3ad2ant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> C C_ On )
91 90 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> C C_ On )
92 xpss12 
 |-  ( ( { ( A +no B ) } C_ On /\ C C_ On ) -> ( { ( A +no B ) } X. C ) C_ ( On X. On ) )
93 88 91 92 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { ( A +no B ) } X. C ) C_ ( On X. On ) )
94 93 34 sseqtrrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { ( A +no B ) } X. C ) C_ dom +no )
95 funimassov 
 |-  ( ( Fun +no /\ ( { ( A +no B ) } X. C ) C_ dom +no ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x ) )
96 24 94 95 sylancr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x ) )
97 ovex 
 |-  ( A +no B ) e. _V
98 oveq1 
 |-  ( a = ( A +no B ) -> ( a +no c ) = ( ( A +no B ) +no c ) )
99 98 eleq1d 
 |-  ( a = ( A +no B ) -> ( ( a +no c ) e. x <-> ( ( A +no B ) +no c ) e. x ) )
100 99 ralbidv 
 |-  ( a = ( A +no B ) -> ( A. c e. C ( a +no c ) e. x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) )
101 97 100 ralsn 
 |-  ( A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x <-> A. c e. C ( ( A +no B ) +no c ) e. x )
102 96 101 bitrdi 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) )
103 61 86 102 3anbi123d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) ) )
104 21 103 bitrid 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x <-> ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) ) )
105 104 rabbidva 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } = { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } )
106 105 inteqd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> |^| { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } )
107 9 106 eqtrd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } )