This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ⊆ ( ... ‘ 𝑋 ) ) )