Axiom ax-arg 1153

Description: The Arguesian law as an axiom. (Contributed by NM, 1-Apr-2012.)

Hypothesis

Ref	Expression
arg.1	((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2)

Assertion

Ref	Expression
ax-arg	((a0 ∪ a1) ∩ (b0 ∪ b1)) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))

Detailed syntax breakdown of Axiom ax-arg

Step	Hyp	Ref	Expression
1		wva0	. . . 4 term  a0
2		wva1	. . . 4 term  a1
3	1, 2	wo 6	. . 3 term  (a0 ∪ a1)
4		wvb0	. . . 4 term  b0
5		wvb1	. . . 4 term  b1
6	4, 5	wo 6	. . 3 term  (b0 ∪ b1)
7	3, 6	wa 7	. 2 term  ((a0 ∪ a1) ∩ (b0 ∪ b1))
8		wva2	. . . . 5 term  a2
9	1, 8	wo 6	. . . 4 term  (a0 ∪ a2)
10		wvb2	. . . . 5 term  b2
11	4, 10	wo 6	. . . 4 term  (b0 ∪ b2)
12	9, 11	wa 7	. . 3 term  ((a0 ∪ a2) ∩ (b0 ∪ b2))
13	2, 8	wo 6	. . . 4 term  (a1 ∪ a2)
14	5, 10	wo 6	. . . 4 term  (b1 ∪ b2)
15	13, 14	wa 7	. . 3 term  ((a1 ∪ a2) ∩ (b1 ∪ b2))
16	12, 15	wo 6	. 2 term  (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))
17	7, 16	wle 2	1 wff  ((a0 ∪ a1) ∩ (b0 ∪ b1)) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))

This axiom is referenced by:  dp15lemb  1155  xdp15  1199  xxdp15  1202