Theorem addscllem1 33774

Description: Lemma for addscl (future) Alternate expression for surreal addition. (Contributed by Scott Fenton, 23-Aug-2024.)

Assertion

Ref	Expression
addscllem1	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = ((( +s “ (( L ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( L ‘𝐵)))) |s (( +s “ (( R ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( R ‘𝐵))))))

Proof of Theorem addscllem1

Dummy variables 𝑙 𝑟 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		addsval 33769	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (({𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)}) |s ({𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)})))
2		addsfn 33768	. . . . . . 7 ⊢ +s Fn ( No × No )
3		leftssno 33706	. . . . . . . . 9 ⊢ ( L ‘𝐴) ⊆ No
4	3	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ No → ( L ‘𝐴) ⊆ No )
5		snssi 4696	. . . . . . . 8 ⊢ (𝐵 ∈ No → {𝐵} ⊆ No )
6		xpss12 5540	. . . . . . . 8 ⊢ ((( L ‘𝐴) ⊆ No ∧ {𝐵} ⊆ No ) → (( L ‘𝐴) × {𝐵}) ⊆ ( No × No ))
7	4, 5, 6	syl2an 599	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( L ‘𝐴) × {𝐵}) ⊆ ( No × No ))
8		ovelimab 7342	. . . . . . 7 ⊢ (( +s Fn ( No × No ) ∧ (( L ‘𝐴) × {𝐵}) ⊆ ( No × No )) → (𝑥 ∈ ( +s “ (( L ‘𝐴) × {𝐵})) ↔ ∃𝑙 ∈ ( L ‘𝐴)∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟)))
9	2, 7, 8	sylancr 590	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑥 ∈ ( +s “ (( L ‘𝐴) × {𝐵})) ↔ ∃𝑙 ∈ ( L ‘𝐴)∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟)))
10		oveq2 7178	. . . . . . . . . 10 ⊢ (𝑟 = 𝐵 → (𝑙 +s 𝑟) = (𝑙 +s 𝐵))
11	10	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑟 = 𝐵 → (𝑥 = (𝑙 +s 𝑟) ↔ 𝑥 = (𝑙 +s 𝐵)))
12	11	rexsng 4565	. . . . . . . 8 ⊢ (𝐵 ∈ No → (∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟) ↔ 𝑥 = (𝑙 +s 𝐵)))
13	12	adantl 485	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟) ↔ 𝑥 = (𝑙 +s 𝐵)))
14	13	rexbidv 3207	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (∃𝑙 ∈ ( L ‘𝐴)∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)))
15	9, 14	bitrd 282	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑥 ∈ ( +s “ (( L ‘𝐴) × {𝐵})) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)))
16	15	abbi2dv 2869	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ (( L ‘𝐴) × {𝐵})) = {𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)})
17		snssi 4696	. . . . . . . 8 ⊢ (𝐴 ∈ No → {𝐴} ⊆ No )
18		leftssno 33706	. . . . . . . . 9 ⊢ ( L ‘𝐵) ⊆ No
19	18	a1i 11	. . . . . . . 8 ⊢ (𝐵 ∈ No → ( L ‘𝐵) ⊆ No )
20		xpss12 5540	. . . . . . . 8 ⊢ (({𝐴} ⊆ No ∧ ( L ‘𝐵) ⊆ No ) → ({𝐴} × ( L ‘𝐵)) ⊆ ( No × No ))
21	17, 19, 20	syl2an 599	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ({𝐴} × ( L ‘𝐵)) ⊆ ( No × No ))
22		ovelimab 7342	. . . . . . 7 ⊢ (( +s Fn ( No × No ) ∧ ({𝐴} × ( L ‘𝐵)) ⊆ ( No × No )) → (𝑦 ∈ ( +s “ ({𝐴} × ( L ‘𝐵))) ↔ ∃𝑟 ∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙)))
23	2, 21, 22	sylancr 590	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( L ‘𝐵))) ↔ ∃𝑟 ∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙)))
24		oveq1 7177	. . . . . . . . . 10 ⊢ (𝑟 = 𝐴 → (𝑟 +s 𝑙) = (𝐴 +s 𝑙))
25	24	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑟 = 𝐴 → (𝑦 = (𝑟 +s 𝑙) ↔ 𝑦 = (𝐴 +s 𝑙)))
26	25	rexbidv 3207	. . . . . . . 8 ⊢ (𝑟 = 𝐴 → (∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)))
27	26	rexsng 4565	. . . . . . 7 ⊢ (𝐴 ∈ No → (∃𝑟 ∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)))
28	27	adantr 484	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (∃𝑟 ∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)))
29	23, 28	bitrd 282	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( L ‘𝐵))) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)))
30	29	abbi2dv 2869	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ ({𝐴} × ( L ‘𝐵))) = {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)})
31	16, 30	uneq12d 4054	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( +s “ (( L ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( L ‘𝐵)))) = ({𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)}))
32		rightssno 33707	. . . . . . . . 9 ⊢ ( R ‘𝐴) ⊆ No
33	32	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ No → ( R ‘𝐴) ⊆ No )
34		xpss12 5540	. . . . . . . 8 ⊢ ((( R ‘𝐴) ⊆ No ∧ {𝐵} ⊆ No ) → (( R ‘𝐴) × {𝐵}) ⊆ ( No × No ))
35	33, 5, 34	syl2an 599	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( R ‘𝐴) × {𝐵}) ⊆ ( No × No ))
36		ovelimab 7342	. . . . . . 7 ⊢ (( +s Fn ( No × No ) ∧ (( R ‘𝐴) × {𝐵}) ⊆ ( No × No )) → (𝑥 ∈ ( +s “ (( R ‘𝐴) × {𝐵})) ↔ ∃𝑟 ∈ ( R ‘𝐴)∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙)))
37	2, 35, 36	sylancr 590	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑥 ∈ ( +s “ (( R ‘𝐴) × {𝐵})) ↔ ∃𝑟 ∈ ( R ‘𝐴)∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙)))
38		oveq2 7178	. . . . . . . . . 10 ⊢ (𝑙 = 𝐵 → (𝑟 +s 𝑙) = (𝑟 +s 𝐵))
39	38	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑙 = 𝐵 → (𝑥 = (𝑟 +s 𝑙) ↔ 𝑥 = (𝑟 +s 𝐵)))
40	39	rexsng 4565	. . . . . . . 8 ⊢ (𝐵 ∈ No → (∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙) ↔ 𝑥 = (𝑟 +s 𝐵)))
41	40	adantl 485	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙) ↔ 𝑥 = (𝑟 +s 𝐵)))
42	41	rexbidv 3207	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (∃𝑟 ∈ ( R ‘𝐴)∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙) ↔ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)))
43	37, 42	bitrd 282	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑥 ∈ ( +s “ (( R ‘𝐴) × {𝐵})) ↔ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)))
44	43	abbi2dv 2869	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ (( R ‘𝐴) × {𝐵})) = {𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)})
45		rightssno 33707	. . . . . . . . 9 ⊢ ( R ‘𝐵) ⊆ No
46	45	a1i 11	. . . . . . . 8 ⊢ (𝐵 ∈ No → ( R ‘𝐵) ⊆ No )
47		xpss12 5540	. . . . . . . 8 ⊢ (({𝐴} ⊆ No ∧ ( R ‘𝐵) ⊆ No ) → ({𝐴} × ( R ‘𝐵)) ⊆ ( No × No ))
48	17, 46, 47	syl2an 599	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ({𝐴} × ( R ‘𝐵)) ⊆ ( No × No ))
49		ovelimab 7342	. . . . . . 7 ⊢ (( +s Fn ( No × No ) ∧ ({𝐴} × ( R ‘𝐵)) ⊆ ( No × No )) → (𝑦 ∈ ( +s “ ({𝐴} × ( R ‘𝐵))) ↔ ∃𝑙 ∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟)))
50	2, 48, 49	sylancr 590	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( R ‘𝐵))) ↔ ∃𝑙 ∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟)))
51		oveq1 7177	. . . . . . . . . 10 ⊢ (𝑙 = 𝐴 → (𝑙 +s 𝑟) = (𝐴 +s 𝑟))
52	51	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑙 = 𝐴 → (𝑦 = (𝑙 +s 𝑟) ↔ 𝑦 = (𝐴 +s 𝑟)))
53	52	rexbidv 3207	. . . . . . . 8 ⊢ (𝑙 = 𝐴 → (∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)))
54	53	rexsng 4565	. . . . . . 7 ⊢ (𝐴 ∈ No → (∃𝑙 ∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)))
55	54	adantr 484	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (∃𝑙 ∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)))
56	50, 55	bitrd 282	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( R ‘𝐵))) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)))
57	56	abbi2dv 2869	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ ({𝐴} × ( R ‘𝐵))) = {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)})
58	44, 57	uneq12d 4054	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( +s “ (( R ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( R ‘𝐵)))) = ({𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)}))
59	31, 58	oveq12d 7188	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((( +s “ (( L ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( L ‘𝐵)))) |s (( +s “ (( R ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( R ‘𝐵))))) = (({𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)}) |s ({𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)})))
60	1, 59	eqtr4d 2776	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = ((( +s “ (( L ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( L ‘𝐵)))) |s (( +s “ (( R ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( R ‘𝐵))))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2114  {cab 2716  ∃wrex 3054   ∪ cun 3841   ⊆ wss 3843  {csn 4516   × cxp 5523   “ cima 5528   Fn wfn 6334  ‘cfv 6339  (class class class)co 7170   No csur 33486   |s cscut 33620   L cleft 33672   R cright 33673   +s cadds 33759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-1o 8131  df-2o 8132  df-frecs 33438  df-no 33489  df-slt 33490  df-bday 33491  df-sslt 33619  df-scut 33621  df-made 33674  df-old 33675  df-left 33677  df-right 33678  df-norec2 33749  df-adds 33762

This theorem is referenced by: (None)