setsstruct

Description: An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 9-Jun-2021) (Revised by AV, 14-Nov-2021)

		Ref	Expression
	Assertion	setsstruct	$⊢ (E \in V \land I \in ℤ_{\geq M} \land G Struct ⟨M, N⟩) \to (G sSet ⟨I, E⟩) Struct ⟨M, if (I \leq N, N, I)⟩$

Proof

Step	Hyp	Ref	Expression
1		isstruct	$⊢ G Struct ⟨M, N⟩ \leftrightarrow ((M \in ℕ \land N \in ℕ \land M \leq N) \land Fun (G ∖ \{\emptyset\}) \land dom G \subseteq (M \dots N))$
2		simp2	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to G Struct ⟨M, N⟩$
3		simp3l	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to E \in V$
4		1z	$⊢ 1 \in ℤ$
5		nnge1	$⊢ M \in ℕ \to 1 \leq M$
6		eluzuzle	$⊢ (1 \in ℤ \land 1 \leq M) \to (I \in ℤ_{\geq M} \to I \in ℤ_{\geq 1})$
7	4 5 6	sylancr	$⊢ M \in ℕ \to (I \in ℤ_{\geq M} \to I \in ℤ_{\geq 1})$
8		elnnuz	$⊢ I \in ℕ \leftrightarrow I \in ℤ_{\geq 1}$
9	7 8	syl6ibr	$⊢ M \in ℕ \to (I \in ℤ_{\geq M} \to I \in ℕ)$
10	9	adantld	$⊢ M \in ℕ \to ((E \in V \land I \in ℤ_{\geq M}) \to I \in ℕ)$
11	10	3ad2ant1	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N) \to ((E \in V \land I \in ℤ_{\geq M}) \to I \in ℕ)$
12	11	a1d	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N) \to (G Struct ⟨M, N⟩ \to ((E \in V \land I \in ℤ_{\geq M}) \to I \in ℕ))$
13	12	3imp	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to I \in ℕ$
14	2 3 13	3jca	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to (G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ)$
15		op1stg	$⊢ (M \in ℕ \land N \in ℕ) \to 1^{st} (⟨M, N⟩) = M$
16	15	breq2d	$⊢ (M \in ℕ \land N \in ℕ) \to (I \leq 1^{st} (⟨M, N⟩) \leftrightarrow I \leq M)$
17		eqidd	$⊢ (M \in ℕ \land N \in ℕ) \to I = I$
18	16 17 15	ifbieq12d	$⊢ (M \in ℕ \land N \in ℕ) \to if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)) = if (I \leq M, I, M)$
19	18	3adant3	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N) \to if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)) = if (I \leq M, I, M)$
20	19	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land (E \in V \land I \in ℤ_{\geq M})) \to if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)) = if (I \leq M, I, M)$
21		eluz2	$⊢ I \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land I \in ℤ \land M \leq I)$
22		zre	$⊢ I \in ℤ \to I \in ℝ$
23	22	rexrd	$⊢ I \in ℤ \to I \in ℝ^{*}$
24	23	3ad2ant2	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to I \in ℝ^{*}$
25		zre	$⊢ M \in ℤ \to M \in ℝ$
26	25	rexrd	$⊢ M \in ℤ \to M \in ℝ^{*}$
27	26	3ad2ant1	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to M \in ℝ^{*}$
28		simp3	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to M \leq I$
29	24 27 28	3jca	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to (I \in ℝ^{} \land M \in ℝ^{} \land M \leq I)$
30	29	a1d	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to ((M \in ℕ \land N \in ℕ \land M \leq N) \to (I \in ℝ^{} \land M \in ℝ^{} \land M \leq I))$
31	21 30	sylbi	$⊢ I \in ℤ_{\geq M} \to ((M \in ℕ \land N \in ℕ \land M \leq N) \to (I \in ℝ^{} \land M \in ℝ^{} \land M \leq I))$
32	31	adantl	$⊢ (E \in V \land I \in ℤ_{\geq M}) \to ((M \in ℕ \land N \in ℕ \land M \leq N) \to (I \in ℝ^{} \land M \in ℝ^{} \land M \leq I))$
33	32	impcom	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land (E \in V \land I \in ℤ_{\geq M})) \to (I \in ℝ^{} \land M \in ℝ^{} \land M \leq I)$
34		xrmineq	$⊢ (I \in ℝ^{} \land M \in ℝ^{} \land M \leq I) \to if (I \leq M, I, M) = M$
35	33 34	syl	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land (E \in V \land I \in ℤ_{\geq M})) \to if (I \leq M, I, M) = M$
36	20 35	eqtr2d	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land (E \in V \land I \in ℤ_{\geq M})) \to M = if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩))$
37	36	3adant2	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to M = if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩))$
38		op2ndg	$⊢ (M \in ℕ \land N \in ℕ) \to 2^{nd} (⟨M, N⟩) = N$
39	38	eqcomd	$⊢ (M \in ℕ \land N \in ℕ) \to N = 2^{nd} (⟨M, N⟩)$
40	39	breq2d	$⊢ (M \in ℕ \land N \in ℕ) \to (I \leq N \leftrightarrow I \leq 2^{nd} (⟨M, N⟩))$
41	40 39 17	ifbieq12d	$⊢ (M \in ℕ \land N \in ℕ) \to if (I \leq N, N, I) = if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)$
42	41	3adant3	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N) \to if (I \leq N, N, I) = if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)$
43	42	3ad2ant1	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to if (I \leq N, N, I) = if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)$
44	37 43	opeq12d	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩$
45	14 44	jca	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land G Struct ⟨M, N⟩ \land (E \in V \land I \in ℤ_{\geq M})) \to ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩)$
46	45	3exp	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N) \to (G Struct ⟨M, N⟩ \to ((E \in V \land I \in ℤ_{\geq M}) \to ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩)))$
47	46	3ad2ant1	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land Fun (G ∖ \{\emptyset\}) \land dom G \subseteq (M \dots N)) \to (G Struct ⟨M, N⟩ \to ((E \in V \land I \in ℤ_{\geq M}) \to ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩)))$
48	1 47	sylbi	$⊢ G Struct ⟨M, N⟩ \to (G Struct ⟨M, N⟩ \to ((E \in V \land I \in ℤ_{\geq M}) \to ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩)))$
49	48	pm2.43i	$⊢ G Struct ⟨M, N⟩ \to ((E \in V \land I \in ℤ_{\geq M}) \to ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩))$
50	49	expdcom	$⊢ E \in V \to (I \in ℤ_{\geq M} \to (G Struct ⟨M, N⟩ \to ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩)))$
51	50	3imp	$⊢ (E \in V \land I \in ℤ_{\geq M} \land G Struct ⟨M, N⟩) \to ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩)$
52		setsstruct2	$⊢ ((G Struct ⟨M, N⟩ \land E \in V \land I \in ℕ) \land ⟨M, if (I \leq N, N, I)⟩ = ⟨if (I \leq 1^{st} (⟨M, N⟩), I, 1^{st} (⟨M, N⟩)), if (I \leq 2^{nd} (⟨M, N⟩), 2^{nd} (⟨M, N⟩), I)⟩) \to (G sSet ⟨I, E⟩) Struct ⟨M, if (I \leq N, N, I)⟩$
53	51 52	syl	$⊢ (E \in V \land I \in ℤ_{\geq M} \land G Struct ⟨M, N⟩) \to (G sSet ⟨I, E⟩) Struct ⟨M, if (I \leq N, N, I)⟩$

Metamath Proof Explorer

Theorem setsstruct

Proof