Theorem usgredgsscusgredg

Description: A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 13-Nov-2020)

	Ref	Expression
Hypotheses	fusgrmaxsize.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	fusgrmaxsize.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	usgrsscusgra.h	⊢ 𝑉 = ( Vtx ‘ 𝐻 )
	usgrsscusgra.f	⊢ 𝐹 = ( Edg ‘ 𝐻 )
Assertion	usgredgsscusgredg	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → 𝐸 ⊆ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fusgrmaxsize.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgrmaxsize.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		usgrsscusgra.h	⊢ 𝑉 = ( Vtx ‘ 𝐻 )
4		usgrsscusgra.f	⊢ 𝐹 = ( Edg ‘ 𝐻 )
5	1 2	usgredg	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) )
6	3 4	iscusgredg	⊢ ( 𝐻 ∈ ComplUSGraph ↔ ( 𝐻 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ) )
7		sneq	⊢ ( 𝑘 = 𝑎 → { 𝑘 } = { 𝑎 } )
8	7	difeq2d	⊢ ( 𝑘 = 𝑎 → ( 𝑉 ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝑎 } ) )
9		preq2	⊢ ( 𝑘 = 𝑎 → { 𝑛 , 𝑘 } = { 𝑛 , 𝑎 } )
10	9	eleq1d	⊢ ( 𝑘 = 𝑎 → ( { 𝑛 , 𝑘 } ∈ 𝐹 ↔ { 𝑛 , 𝑎 } ∈ 𝐹 ) )
11	8 10	raleqbidv	⊢ ( 𝑘 = 𝑎 → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 ) )
12	11	rspcv	⊢ ( 𝑎 ∈ 𝑉 → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 ) )
13		simpl	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 )
14	13	necomd	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → 𝑏 ≠ 𝑎 )
15	14	anim2i	⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( 𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎 ) )
16		eldifsn	⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ↔ ( 𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎 ) )
17	15 16	sylibr	⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) )
18		preq1	⊢ ( 𝑛 = 𝑏 → { 𝑛 , 𝑎 } = { 𝑏 , 𝑎 } )
19	18	eleq1d	⊢ ( 𝑛 = 𝑏 → ( { 𝑛 , 𝑎 } ∈ 𝐹 ↔ { 𝑏 , 𝑎 } ∈ 𝐹 ) )
20	19	rspcv	⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → { 𝑏 , 𝑎 } ∈ 𝐹 ) )
21	17 20	syl	⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → { 𝑏 , 𝑎 } ∈ 𝐹 ) )
22		prcom	⊢ { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 }
23	22	eqeq2i	⊢ ( 𝑒 = { 𝑎 , 𝑏 } ↔ 𝑒 = { 𝑏 , 𝑎 } )
24		eqcom	⊢ ( 𝑒 = { 𝑏 , 𝑎 } ↔ { 𝑏 , 𝑎 } = 𝑒 )
25	23 24	sylbb	⊢ ( 𝑒 = { 𝑎 , 𝑏 } → { 𝑏 , 𝑎 } = 𝑒 )
26	25	eleq1d	⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ∈ 𝐹 ↔ 𝑒 ∈ 𝐹 ) )
27	26	biimpd	⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
28	27	ad2antll	⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( { 𝑏 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
29	21 28	syld	⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
30	12 29	syl9	⊢ ( 𝑎 ∈ 𝑉 → ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) ) )
31	30	impl	⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
32	31	adantld	⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ( 𝐻 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ) → 𝑒 ∈ 𝐹 ) )
33	6 32	syl5bi	⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) )
34	33	ex	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) ) )
35	34	rexlimivv	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) )
36	5 35	syl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸 ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) )
37	36	impancom	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( 𝑒 ∈ 𝐸 → 𝑒 ∈ 𝐹 ) )
38	37	ssrdv	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → 𝐸 ⊆ 𝐹 )