Theorem isstruct2

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

	Ref	Expression
Assertion	isstruct2	⊢ ( 𝐹 Struct 𝑋 ↔ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brstruct	⊢ Rel Struct
2	1	brrelex12i	⊢ ( 𝐹 Struct 𝑋 → ( 𝐹 ∈ V ∧ 𝑋 ∈ V ) )
3		ssun1	⊢ 𝐹 ⊆ ( 𝐹 ∪ { ∅ } )
4		undif1	⊢ ( ( 𝐹 ∖ { ∅ } ) ∪ { ∅ } ) = ( 𝐹 ∪ { ∅ } )
5	3 4	sseqtrri	⊢ 𝐹 ⊆ ( ( 𝐹 ∖ { ∅ } ) ∪ { ∅ } )
6		simp2	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → Fun ( 𝐹 ∖ { ∅ } ) )
7	6	funfnd	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → ( 𝐹 ∖ { ∅ } ) Fn dom ( 𝐹 ∖ { ∅ } ) )
8		elinel2	⊢ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) → 𝑋 ∈ ( ℕ × ℕ ) )
9		1st2nd2	⊢ ( 𝑋 ∈ ( ℕ × ℕ ) → 𝑋 = ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ )
10	8 9	syl	⊢ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) → 𝑋 = ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ )
11	10	3ad2ant1	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → 𝑋 = ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ )
12	11	fveq2d	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → ( ... ‘ 𝑋 ) = ( ... ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) )
13		df-ov	⊢ ( ( 1st ‘ 𝑋 ) ... ( 2nd ‘ 𝑋 ) ) = ( ... ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ )
14		fzfi	⊢ ( ( 1st ‘ 𝑋 ) ... ( 2nd ‘ 𝑋 ) ) ∈ Fin
15	13 14	eqeltrri	⊢ ( ... ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) ∈ Fin
16	12 15	eqeltrdi	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → ( ... ‘ 𝑋 ) ∈ Fin )
17		difss	⊢ ( 𝐹 ∖ { ∅ } ) ⊆ 𝐹
18		dmss	⊢ ( ( 𝐹 ∖ { ∅ } ) ⊆ 𝐹 → dom ( 𝐹 ∖ { ∅ } ) ⊆ dom 𝐹 )
19	17 18	ax-mp	⊢ dom ( 𝐹 ∖ { ∅ } ) ⊆ dom 𝐹
20		simp3	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → dom 𝐹 ⊆ ( ... ‘ 𝑋 ) )
21	19 20	sstrid	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → dom ( 𝐹 ∖ { ∅ } ) ⊆ ( ... ‘ 𝑋 ) )
22	16 21	ssfid	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → dom ( 𝐹 ∖ { ∅ } ) ∈ Fin )
23		fnfi	⊢ ( ( ( 𝐹 ∖ { ∅ } ) Fn dom ( 𝐹 ∖ { ∅ } ) ∧ dom ( 𝐹 ∖ { ∅ } ) ∈ Fin ) → ( 𝐹 ∖ { ∅ } ) ∈ Fin )
24	7 22 23	syl2anc	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → ( 𝐹 ∖ { ∅ } ) ∈ Fin )
25		p0ex	⊢ { ∅ } ∈ V
26		unexg	⊢ ( ( ( 𝐹 ∖ { ∅ } ) ∈ Fin ∧ { ∅ } ∈ V ) → ( ( 𝐹 ∖ { ∅ } ) ∪ { ∅ } ) ∈ V )
27	24 25 26	sylancl	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → ( ( 𝐹 ∖ { ∅ } ) ∪ { ∅ } ) ∈ V )
28		ssexg	⊢ ( ( 𝐹 ⊆ ( ( 𝐹 ∖ { ∅ } ) ∪ { ∅ } ) ∧ ( ( 𝐹 ∖ { ∅ } ) ∪ { ∅ } ) ∈ V ) → 𝐹 ∈ V )
29	5 27 28	sylancr	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → 𝐹 ∈ V )
30		elex	⊢ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) → 𝑋 ∈ V )
31	30	3ad2ant1	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → 𝑋 ∈ V )
32	29 31	jca	⊢ ( ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) → ( 𝐹 ∈ V ∧ 𝑋 ∈ V ) )
33		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
34	33	eleq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ↔ 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ) )
35		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → 𝑓 = 𝐹 )
36	35	difeq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( 𝑓 ∖ { ∅ } ) = ( 𝐹 ∖ { ∅ } ) )
37	36	funeqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( Fun ( 𝑓 ∖ { ∅ } ) ↔ Fun ( 𝐹 ∖ { ∅ } ) ) )
38	35	dmeqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → dom 𝑓 = dom 𝐹 )
39	33	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( ... ‘ 𝑥 ) = ( ... ‘ 𝑋 ) )
40	38 39	sseq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( dom 𝑓 ⊆ ( ... ‘ 𝑥 ) ↔ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) )
41	34 37 40	3anbi123d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝑓 ∖ { ∅ } ) ∧ dom 𝑓 ⊆ ( ... ‘ 𝑥 ) ) ↔ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) ) )
42		df-struct	⊢ Struct = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝑓 ∖ { ∅ } ) ∧ dom 𝑓 ⊆ ( ... ‘ 𝑥 ) ) }
43	41 42	brabga	⊢ ( ( 𝐹 ∈ V ∧ 𝑋 ∈ V ) → ( 𝐹 Struct 𝑋 ↔ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) ) )
44	2 32 43	pm5.21nii	⊢ ( 𝐹 Struct 𝑋 ↔ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) )