strleun

Description: Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypotheses	strleun.f	$⊢ F Struct ⟨A, B⟩$
	strleun.g	$⊢ G Struct ⟨C, D⟩$
	strleun.l	$⊢ B < C$
Assertion	strleun	$⊢ (F \cup G) Struct ⟨A, D⟩$

Proof

Step	Hyp	Ref	Expression
1		strleun.f	$⊢ F Struct ⟨A, B⟩$
2		strleun.g	$⊢ G Struct ⟨C, D⟩$
3		strleun.l	$⊢ B < C$
4		isstruct	$⊢ F Struct ⟨A, B⟩ \leftrightarrow ((A \in ℕ \land B \in ℕ \land A \leq B) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (A \dots B))$
5	1 4	mpbi	$⊢ ((A \in ℕ \land B \in ℕ \land A \leq B) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (A \dots B))$
6	5	simp1i	$⊢ (A \in ℕ \land B \in ℕ \land A \leq B)$
7	6	simp1i	$⊢ A \in ℕ$
8		isstruct	$⊢ G Struct ⟨C, D⟩ \leftrightarrow ((C \in ℕ \land D \in ℕ \land C \leq D) \land Fun (G ∖ \{\emptyset\}) \land dom G \subseteq (C \dots D))$
9	2 8	mpbi	$⊢ ((C \in ℕ \land D \in ℕ \land C \leq D) \land Fun (G ∖ \{\emptyset\}) \land dom G \subseteq (C \dots D))$
10	9	simp1i	$⊢ (C \in ℕ \land D \in ℕ \land C \leq D)$
11	10	simp2i	$⊢ D \in ℕ$
12	6	simp3i	$⊢ A \leq B$
13	6	simp2i	$⊢ B \in ℕ$
14	13	nnrei	$⊢ B \in ℝ$
15	10	simp1i	$⊢ C \in ℕ$
16	15	nnrei	$⊢ C \in ℝ$
17	14 16 3	ltleii	$⊢ B \leq C$
18	7	nnrei	$⊢ A \in ℝ$
19	18 14 16	letri	$⊢ (A \leq B \land B \leq C) \to A \leq C$
20	12 17 19	mp2an	$⊢ A \leq C$
21	10	simp3i	$⊢ C \leq D$
22	11	nnrei	$⊢ D \in ℝ$
23	18 16 22	letri	$⊢ (A \leq C \land C \leq D) \to A \leq D$
24	20 21 23	mp2an	$⊢ A \leq D$
25	7 11 24	3pm3.2i	$⊢ (A \in ℕ \land D \in ℕ \land A \leq D)$
26	5	simp2i	$⊢ Fun (F ∖ \{\emptyset\})$
27	9	simp2i	$⊢ Fun (G ∖ \{\emptyset\})$
28	26 27	pm3.2i	$⊢ (Fun (F ∖ \{\emptyset\}) \land Fun (G ∖ \{\emptyset\}))$
29		difss	$⊢ F ∖ \{\emptyset\} \subseteq F$
30		dmss	$⊢ F ∖ \{\emptyset\} \subseteq F \to dom (F ∖ \{\emptyset\}) \subseteq dom F$
31	29 30	ax-mp	$⊢ dom (F ∖ \{\emptyset\}) \subseteq dom F$
32	5	simp3i	$⊢ dom F \subseteq (A \dots B)$
33	31 32	sstri	$⊢ dom (F ∖ \{\emptyset\}) \subseteq (A \dots B)$
34		difss	$⊢ G ∖ \{\emptyset\} \subseteq G$
35		dmss	$⊢ G ∖ \{\emptyset\} \subseteq G \to dom (G ∖ \{\emptyset\}) \subseteq dom G$
36	34 35	ax-mp	$⊢ dom (G ∖ \{\emptyset\}) \subseteq dom G$
37	9	simp3i	$⊢ dom G \subseteq (C \dots D)$
38	36 37	sstri	$⊢ dom (G ∖ \{\emptyset\}) \subseteq (C \dots D)$
39		ss2in	$⊢ (dom (F ∖ \{\emptyset\}) \subseteq (A \dots B) \land dom (G ∖ \{\emptyset\}) \subseteq (C \dots D)) \to dom (F ∖ \{\emptyset\}) \cap dom (G ∖ \{\emptyset\}) \subseteq (A \dots B) \cap (C \dots D)$
40	33 38 39	mp2an	$⊢ dom (F ∖ \{\emptyset\}) \cap dom (G ∖ \{\emptyset\}) \subseteq (A \dots B) \cap (C \dots D)$
41		fzdisj	$⊢ B < C \to (A \dots B) \cap (C \dots D) = \emptyset$
42	3 41	ax-mp	$⊢ (A \dots B) \cap (C \dots D) = \emptyset$
43		sseq0	$⊢ (dom (F ∖ \{\emptyset\}) \cap dom (G ∖ \{\emptyset\}) \subseteq (A \dots B) \cap (C \dots D) \land (A \dots B) \cap (C \dots D) = \emptyset) \to dom (F ∖ \{\emptyset\}) \cap dom (G ∖ \{\emptyset\}) = \emptyset$
44	40 42 43	mp2an	$⊢ dom (F ∖ \{\emptyset\}) \cap dom (G ∖ \{\emptyset\}) = \emptyset$
45		funun	$⊢ ((Fun (F ∖ \{\emptyset\}) \land Fun (G ∖ \{\emptyset\})) \land dom (F ∖ \{\emptyset\}) \cap dom (G ∖ \{\emptyset\}) = \emptyset) \to Fun ((F ∖ \{\emptyset\}) \cup (G ∖ \{\emptyset\}))$
46	28 44 45	mp2an	$⊢ Fun ((F ∖ \{\emptyset\}) \cup (G ∖ \{\emptyset\}))$
47		difundir	$⊢ (F \cup G) ∖ \{\emptyset\} = (F ∖ \{\emptyset\}) \cup (G ∖ \{\emptyset\})$
48	47	funeqi	$⊢ Fun ((F \cup G) ∖ \{\emptyset\}) \leftrightarrow Fun ((F ∖ \{\emptyset\}) \cup (G ∖ \{\emptyset\}))$
49	46 48	mpbir	$⊢ Fun ((F \cup G) ∖ \{\emptyset\})$
50		dmun	$⊢ dom (F \cup G) = dom F \cup dom G$
51	13	nnzi	$⊢ B \in ℤ$
52	11	nnzi	$⊢ D \in ℤ$
53	14 16 22	letri	$⊢ (B \leq C \land C \leq D) \to B \leq D$
54	17 21 53	mp2an	$⊢ B \leq D$
55		eluz2	$⊢ D \in ℤ_{\geq B} \leftrightarrow (B \in ℤ \land D \in ℤ \land B \leq D)$
56	51 52 54 55	mpbir3an	$⊢ D \in ℤ_{\geq B}$
57		fzss2	$⊢ D \in ℤ_{\geq B} \to (A \dots B) \subseteq (A \dots D)$
58	56 57	ax-mp	$⊢ (A \dots B) \subseteq (A \dots D)$
59	32 58	sstri	$⊢ dom F \subseteq (A \dots D)$
60	7	nnzi	$⊢ A \in ℤ$
61	15	nnzi	$⊢ C \in ℤ$
62		eluz2	$⊢ C \in ℤ_{\geq A} \leftrightarrow (A \in ℤ \land C \in ℤ \land A \leq C)$
63	60 61 20 62	mpbir3an	$⊢ C \in ℤ_{\geq A}$
64		fzss1	$⊢ C \in ℤ_{\geq A} \to (C \dots D) \subseteq (A \dots D)$
65	63 64	ax-mp	$⊢ (C \dots D) \subseteq (A \dots D)$
66	37 65	sstri	$⊢ dom G \subseteq (A \dots D)$
67	59 66	unssi	$⊢ dom F \cup dom G \subseteq (A \dots D)$
68	50 67	eqsstri	$⊢ dom (F \cup G) \subseteq (A \dots D)$
69		isstruct	$⊢ (F \cup G) Struct ⟨A, D⟩ \leftrightarrow ((A \in ℕ \land D \in ℕ \land A \leq D) \land Fun ((F \cup G) ∖ \{\emptyset\}) \land dom (F \cup G) \subseteq (A \dots D))$
70	25 49 68 69	mpbir3an	$⊢ (F \cup G) Struct ⟨A, D⟩$

Metamath Proof Explorer

Theorem strleun

Proof