strle1

Description: Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypotheses	strle1.i	⊢ 𝐼 ∈ ℕ
	strle1.a	⊢ 𝐴 = 𝐼
Assertion	strle1	⊢ { ⟨ 𝐴 , 𝑋 ⟩ } Struct ⟨ 𝐼 , 𝐼 ⟩

Proof

Step	Hyp	Ref	Expression
1		strle1.i	⊢ 𝐼 ∈ ℕ
2		strle1.a	⊢ 𝐴 = 𝐼
3	1	nnrei	⊢ 𝐼 ∈ ℝ
4	3	leidi	⊢ 𝐼 ≤ 𝐼
5	1 1 4	3pm3.2i	⊢ ( 𝐼 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼 ≤ 𝐼 )
6		difss	⊢ ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) ⊆ { ⟨ 𝐴 , 𝑋 ⟩ }
7	2 1	eqeltri	⊢ 𝐴 ∈ ℕ
8		funsng	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑋 ∈ V ) → Fun { ⟨ 𝐴 , 𝑋 ⟩ } )
9	7 8	mpan	⊢ ( 𝑋 ∈ V → Fun { ⟨ 𝐴 , 𝑋 ⟩ } )
10		funss	⊢ ( ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) ⊆ { ⟨ 𝐴 , 𝑋 ⟩ } → ( Fun { ⟨ 𝐴 , 𝑋 ⟩ } → Fun ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) ) )
11	6 9 10	mpsyl	⊢ ( 𝑋 ∈ V → Fun ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) )
12		fun0	⊢ Fun ∅
13		opprc2	⊢ ( ¬ 𝑋 ∈ V → ⟨ 𝐴 , 𝑋 ⟩ = ∅ )
14	13	sneqd	⊢ ( ¬ 𝑋 ∈ V → { ⟨ 𝐴 , 𝑋 ⟩ } = { ∅ } )
15	14	difeq1d	⊢ ( ¬ 𝑋 ∈ V → ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) = ( { ∅ } ∖ { ∅ } ) )
16		difid	⊢ ( { ∅ } ∖ { ∅ } ) = ∅
17	15 16	eqtrdi	⊢ ( ¬ 𝑋 ∈ V → ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) = ∅ )
18	17	funeqd	⊢ ( ¬ 𝑋 ∈ V → ( Fun ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) ↔ Fun ∅ ) )
19	12 18	mpbiri	⊢ ( ¬ 𝑋 ∈ V → Fun ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) )
20	11 19	pm2.61i	⊢ Fun ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } )
21		dmsnopss	⊢ dom { ⟨ 𝐴 , 𝑋 ⟩ } ⊆ { 𝐴 }
22	2	sneqi	⊢ { 𝐴 } = { 𝐼 }
23	1	nnzi	⊢ 𝐼 ∈ ℤ
24		fzsn	⊢ ( 𝐼 ∈ ℤ → ( 𝐼 ... 𝐼 ) = { 𝐼 } )
25	23 24	ax-mp	⊢ ( 𝐼 ... 𝐼 ) = { 𝐼 }
26	22 25	eqtr4i	⊢ { 𝐴 } = ( 𝐼 ... 𝐼 )
27	21 26	sseqtri	⊢ dom { ⟨ 𝐴 , 𝑋 ⟩ } ⊆ ( 𝐼 ... 𝐼 )
28		isstruct	⊢ ( { ⟨ 𝐴 , 𝑋 ⟩ } Struct ⟨ 𝐼 , 𝐼 ⟩ ↔ ( ( 𝐼 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼 ≤ 𝐼 ) ∧ Fun ( { ⟨ 𝐴 , 𝑋 ⟩ } ∖ { ∅ } ) ∧ dom { ⟨ 𝐴 , 𝑋 ⟩ } ⊆ ( 𝐼 ... 𝐼 ) ) )
29	5 20 27 28	mpbir3an	⊢ { ⟨ 𝐴 , 𝑋 ⟩ } Struct ⟨ 𝐼 , 𝐼 ⟩

Metamath Proof Explorer

Theorem strle1

Proof