paddasslem17 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > paddasslem17		Structured version Visualization version GIF version

Theorem paddasslem17 35995

Description: Lemma for paddass 35997. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.)

**Hypotheses**
Ref	Expression
paddass.a	⊢ 𝐴 = (Atoms‘𝐾)
paddass.p	⊢ + = (+_𝑃‘𝐾)

**Assertion**
Ref	Expression
paddasslem17	⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))

**Proof of Theorem paddasslem17**
Step	Hyp	Ref	Expression
1		ianor 967	. . . 4 ⊢ (¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ↔ (¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∨ ¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)))
2		ianor 967	. . . . . 6 ⊢ (¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ↔ (¬ 𝑋 ≠ ∅ ∨ ¬ (𝑌 + 𝑍) ≠ ∅))
3		nne 2973	. . . . . . 7 ⊢ (¬ 𝑋 ≠ ∅ ↔ 𝑋 = ∅)
4		nne 2973	. . . . . . 7 ⊢ (¬ (𝑌 + 𝑍) ≠ ∅ ↔ (𝑌 + 𝑍) = ∅)
5	3, 4	orbi12i 901	. . . . . 6 ⊢ ((¬ 𝑋 ≠ ∅ ∨ ¬ (𝑌 + 𝑍) ≠ ∅) ↔ (𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅))
6	2, 5	bitri 267	. . . . 5 ⊢ (¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ↔ (𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅))
7		ianor 967	. . . . . 6 ⊢ (¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅) ↔ (¬ 𝑌 ≠ ∅ ∨ ¬ 𝑍 ≠ ∅))
8		nne 2973	. . . . . . 7 ⊢ (¬ 𝑌 ≠ ∅ ↔ 𝑌 = ∅)
9		nne 2973	. . . . . . 7 ⊢ (¬ 𝑍 ≠ ∅ ↔ 𝑍 = ∅)
10	8, 9	orbi12i 901	. . . . . 6 ⊢ ((¬ 𝑌 ≠ ∅ ∨ ¬ 𝑍 ≠ ∅) ↔ (𝑌 = ∅ ∨ 𝑍 = ∅))
11	7, 10	bitri 267	. . . . 5 ⊢ (¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅) ↔ (𝑌 = ∅ ∨ 𝑍 = ∅))
12	6, 11	orbi12i 901	. . . 4 ⊢ ((¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∨ ¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ↔ ((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) ∨ (𝑌 = ∅ ∨ 𝑍 = ∅)))
13	1, 12	bitri 267	. . 3 ⊢ (¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ↔ ((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) ∨ (𝑌 = ∅ ∨ 𝑍 = ∅)))
14		paddass.a	. . . . . . . . . . 11 ⊢ 𝐴 = (Atoms‘𝐾)
15		paddass.p	. . . . . . . . . . 11 ⊢ + = (+_𝑃‘𝐾)
16	14, 15	paddssat 35973	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 + 𝑍) ⊆ 𝐴)
17	16	3adant3r1 1190	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + 𝑍) ⊆ 𝐴)
18	14, 15	padd02 35971	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑌 + 𝑍) ⊆ 𝐴) → (∅ + (𝑌 + 𝑍)) = (𝑌 + 𝑍))
19	17, 18	syldan 585	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + (𝑌 + 𝑍)) = (𝑌 + 𝑍))
20	14, 15	padd02 35971	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴) → (∅ + 𝑌) = 𝑌)
21	20	3ad2antr2 1197	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + 𝑌) = 𝑌)
22	21	oveq1d 6939	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((∅ + 𝑌) + 𝑍) = (𝑌 + 𝑍))
23	19, 22	eqtr4d 2817	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + (𝑌 + 𝑍)) = ((∅ + 𝑌) + 𝑍))
24		oveq1 6931	. . . . . . . 8 ⊢ (𝑋 = ∅ → (𝑋 + (𝑌 + 𝑍)) = (∅ + (𝑌 + 𝑍)))
25		oveq1 6931	. . . . . . . . 9 ⊢ (𝑋 = ∅ → (𝑋 + 𝑌) = (∅ + 𝑌))
26	25	oveq1d 6939	. . . . . . . 8 ⊢ (𝑋 = ∅ → ((𝑋 + 𝑌) + 𝑍) = ((∅ + 𝑌) + 𝑍))
27	24, 26	eqeq12d 2793	. . . . . . 7 ⊢ (𝑋 = ∅ → ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) ↔ (∅ + (𝑌 + 𝑍)) = ((∅ + 𝑌) + 𝑍)))
28	23, 27	syl5ibrcom 239	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 = ∅ → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
29		eqimss 3876	. . . . . 6 ⊢ ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
30	28, 29	syl6 35	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 = ∅ → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
31	14, 15	padd01 35970	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 + ∅) = 𝑋)
32	31	3ad2antr1 1196	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + ∅) = 𝑋)
33	14, 15	sspadd1 35974	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + 𝑌))
34	33	3adant3r3 1192	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ⊆ (𝑋 + 𝑌))
35		simpl 476	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝐾 ∈ HL)
36	14, 15	paddssat 35973	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)
37	36	3adant3r3 1192	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + 𝑌) ⊆ 𝐴)
38		simpr3 1209	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑍 ⊆ 𝐴)
39	14, 15	sspadd1 35974	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ ((𝑋 + 𝑌) + 𝑍))
40	35, 37, 38, 39	syl3anc 1439	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + 𝑌) ⊆ ((𝑋 + 𝑌) + 𝑍))
41	34, 40	sstrd 3831	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ⊆ ((𝑋 + 𝑌) + 𝑍))
42	32, 41	eqsstrd 3858	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + ∅) ⊆ ((𝑋 + 𝑌) + 𝑍))
43		oveq2 6932	. . . . . . 7 ⊢ ((𝑌 + 𝑍) = ∅ → (𝑋 + (𝑌 + 𝑍)) = (𝑋 + ∅))
44	43	sseq1d 3851	. . . . . 6 ⊢ ((𝑌 + 𝑍) = ∅ → ((𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍) ↔ (𝑋 + ∅) ⊆ ((𝑋 + 𝑌) + 𝑍)))
45	42, 44	syl5ibrcom 239	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑌 + 𝑍) = ∅ → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
46	30, 45	jaod 848	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
47	14, 15	padd02 35971	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴) → (∅ + 𝑍) = 𝑍)
48	47	3ad2antr3 1198	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + 𝑍) = 𝑍)
49	48	oveq2d 6940	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (∅ + 𝑍)) = (𝑋 + 𝑍))
50	32	oveq1d 6939	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + ∅) + 𝑍) = (𝑋 + 𝑍))
51	49, 50	eqtr4d 2817	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (∅ + 𝑍)) = ((𝑋 + ∅) + 𝑍))
52		oveq1 6931	. . . . . . . . 9 ⊢ (𝑌 = ∅ → (𝑌 + 𝑍) = (∅ + 𝑍))
53	52	oveq2d 6940	. . . . . . . 8 ⊢ (𝑌 = ∅ → (𝑋 + (𝑌 + 𝑍)) = (𝑋 + (∅ + 𝑍)))
54		oveq2 6932	. . . . . . . . 9 ⊢ (𝑌 = ∅ → (𝑋 + 𝑌) = (𝑋 + ∅))
55	54	oveq1d 6939	. . . . . . . 8 ⊢ (𝑌 = ∅ → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + ∅) + 𝑍))
56	53, 55	eqeq12d 2793	. . . . . . 7 ⊢ (𝑌 = ∅ → ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) ↔ (𝑋 + (∅ + 𝑍)) = ((𝑋 + ∅) + 𝑍)))
57	51, 56	syl5ibrcom 239	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 = ∅ → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
58	14, 15	padd01 35970	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴) → (𝑌 + ∅) = 𝑌)
59	58	3ad2antr2 1197	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + ∅) = 𝑌)
60	59	oveq2d 6940	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + ∅)) = (𝑋 + 𝑌))
61	14, 15	padd01 35970	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴) → ((𝑋 + 𝑌) + ∅) = (𝑋 + 𝑌))
62	37, 61	syldan 585	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + ∅) = (𝑋 + 𝑌))
63	60, 62	eqtr4d 2817	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + ∅)) = ((𝑋 + 𝑌) + ∅))
64		oveq2 6932	. . . . . . . . 9 ⊢ (𝑍 = ∅ → (𝑌 + 𝑍) = (𝑌 + ∅))
65	64	oveq2d 6940	. . . . . . . 8 ⊢ (𝑍 = ∅ → (𝑋 + (𝑌 + 𝑍)) = (𝑋 + (𝑌 + ∅)))
66		oveq2 6932	. . . . . . . 8 ⊢ (𝑍 = ∅ → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) + ∅))
67	65, 66	eqeq12d 2793	. . . . . . 7 ⊢ (𝑍 = ∅ → ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) ↔ (𝑋 + (𝑌 + ∅)) = ((𝑋 + 𝑌) + ∅)))
68	63, 67	syl5ibrcom 239	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑍 = ∅ → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
69	57, 68	jaod 848	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑌 = ∅ ∨ 𝑍 = ∅) → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
70	69, 29	syl6 35	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑌 = ∅ ∨ 𝑍 = ∅) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
71	46, 70	jaod 848	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) ∨ (𝑌 = ∅ ∨ 𝑍 = ∅)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
72	13, 71	syl5bi 234	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
73	72	3impia 1106	1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 ∨ wo 836 ∧ w3a 1071 = wceq 1601 ∈ wcel 2107 ≠ wne 2969 ⊆ wss 3792 ∅c0 4141 ‘cfv 6137 (class class class)co 6924 Atomscatm 35422 HLchlt 35509 +_𝑃cpadd 35954

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5008 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-iun 4757 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 df-ov 6927 df-oprab 6928 df-mpt2 6929 df-1st 7447 df-2nd 7448 df-padd 35955

This theorem is referenced by: paddasslem18 35996

W3C validator