Theorem cntzrecd

Description: Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	cntzrecd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	cntzrecd.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
	cntzrecd.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
	cntzrecd.s	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
Assertion	cntzrecd	⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		cntzrecd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2		cntzrecd.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
3		cntzrecd.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
4		cntzrecd.s	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	5	subgss	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
7	5	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
8	5 1	cntzrec	⊢ ( ( 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ↔ 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
9	6 7 8	syl2an	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ↔ 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
10	2 3 9	syl2anc	⊢ ( 𝜑 → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ↔ 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) ) )
11	4 10	mpbid	⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) )