isstruct2

Description: The property of being a structure with components in ( 1stX ) ... ( 2ndX ) . (Contributed by Mario Carneiro, 29-Aug-2015)

		Ref	Expression
	Assertion	isstruct2	$⊢ F Struct X \leftrightarrow (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X))$

Proof

Step	Hyp	Ref	Expression
1		brstruct	$⊢ Rel Struct$
2	1	brrelex12i	$⊢ F Struct X \to (F \in V \land X \in V)$
3		ssun1	$⊢ F \subseteq F \cup \{\emptyset\}$
4		undif1	$⊢ (F ∖ \{\emptyset\}) \cup \{\emptyset\} = F \cup \{\emptyset\}$
5	3 4	sseqtrri	$⊢ F \subseteq (F ∖ \{\emptyset\}) \cup \{\emptyset\}$
6		simp2	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to Fun (F ∖ \{\emptyset\})$
7	6	funfnd	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to (F ∖ \{\emptyset\}) Fn dom (F ∖ \{\emptyset\})$
8		elinel2	$⊢ X \in (\leq \cap (ℕ \times ℕ)) \to X \in (ℕ \times ℕ)$
9		1st2nd2	$⊢ X \in (ℕ \times ℕ) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
10	8 9	syl	$⊢ X \in (\leq \cap (ℕ \times ℕ)) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
11	10	3ad2ant1	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
12	11	fveq2d	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to \dots (X) = \dots (⟨1^{st} (X), 2^{nd} (X)⟩)$
13		df-ov	$⊢ (1^{st} (X) \dots 2^{nd} (X)) = \dots (⟨1^{st} (X), 2^{nd} (X)⟩)$
14		fzfi	$⊢ (1^{st} (X) \dots 2^{nd} (X)) \in Fin$
15	13 14	eqeltrri	$⊢ \dots (⟨1^{st} (X), 2^{nd} (X)⟩) \in Fin$
16	12 15	eqeltrdi	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to \dots (X) \in Fin$
17		difss	$⊢ F ∖ \{\emptyset\} \subseteq F$
18		dmss	$⊢ F ∖ \{\emptyset\} \subseteq F \to dom (F ∖ \{\emptyset\}) \subseteq dom F$
19	17 18	ax-mp	$⊢ dom (F ∖ \{\emptyset\}) \subseteq dom F$
20		simp3	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to dom F \subseteq \dots (X)$
21	19 20	sstrid	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to dom (F ∖ \{\emptyset\}) \subseteq \dots (X)$
22	16 21	ssfid	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to dom (F ∖ \{\emptyset\}) \in Fin$
23		fnfi	$⊢ ((F ∖ \{\emptyset\}) Fn dom (F ∖ \{\emptyset\}) \land dom (F ∖ \{\emptyset\}) \in Fin) \to F ∖ \{\emptyset\} \in Fin$
24	7 22 23	syl2anc	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to F ∖ \{\emptyset\} \in Fin$
25		p0ex	$⊢ \{\emptyset\} \in V$
26		unexg	$⊢ (F ∖ \{\emptyset\} \in Fin \land \{\emptyset\} \in V) \to (F ∖ \{\emptyset\}) \cup \{\emptyset\} \in V$
27	24 25 26	sylancl	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to (F ∖ \{\emptyset\}) \cup \{\emptyset\} \in V$
28		ssexg	$⊢ (F \subseteq (F ∖ \{\emptyset\}) \cup \{\emptyset\} \land (F ∖ \{\emptyset\}) \cup \{\emptyset\} \in V) \to F \in V$
29	5 27 28	sylancr	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to F \in V$
30		elex	$⊢ X \in (\leq \cap (ℕ \times ℕ)) \to X \in V$
31	30	3ad2ant1	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to X \in V$
32	29 31	jca	$⊢ (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)) \to (F \in V \land X \in V)$
33		simpr	$⊢ (f = F \land x = X) \to x = X$
34	33	eleq1d	$⊢ (f = F \land x = X) \to (x \in (\leq \cap (ℕ \times ℕ)) \leftrightarrow X \in (\leq \cap (ℕ \times ℕ)))$
35		simpl	$⊢ (f = F \land x = X) \to f = F$
36	35	difeq1d	$⊢ (f = F \land x = X) \to f ∖ \{\emptyset\} = F ∖ \{\emptyset\}$
37	36	funeqd	$⊢ (f = F \land x = X) \to (Fun (f ∖ \{\emptyset\}) \leftrightarrow Fun (F ∖ \{\emptyset\}))$
38	35	dmeqd	$⊢ (f = F \land x = X) \to dom f = dom F$
39	33	fveq2d	$⊢ (f = F \land x = X) \to \dots (x) = \dots (X)$
40	38 39	sseq12d	$⊢ (f = F \land x = X) \to (dom f \subseteq \dots (x) \leftrightarrow dom F \subseteq \dots (X))$
41	34 37 40	3anbi123d	$⊢ (f = F \land x = X) \to ((x \in (\leq \cap (ℕ \times ℕ)) \land Fun (f ∖ \{\emptyset\}) \land dom f \subseteq \dots (x)) \leftrightarrow (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)))$
42		df-struct	$⊢ Struct = \{⟨f, x⟩ \| (x \in (\leq \cap (ℕ \times ℕ)) \land Fun (f ∖ \{\emptyset\}) \land dom f \subseteq \dots (x))\}$
43	41 42	brabga	$⊢ (F \in V \land X \in V) \to (F Struct X \leftrightarrow (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X)))$
44	2 32 43	pm5.21nii	$⊢ F Struct X \leftrightarrow (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X))$

Metamath Proof Explorer

Theorem isstruct2

Proof