Theorem cotrintab

Description: The intersection of a class is a transitive relation if membership in the class implies the member is a transitive relation. (Contributed by RP, 28-Oct-2020)

	Ref	Expression
Hypothesis	cotrintab.min	⊢ ( 𝜑 → ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 )
Assertion	cotrintab	⊢ ( ∩ { 𝑥 ∣ 𝜑 } ∘ ∩ { 𝑥 ∣ 𝜑 } ) ⊆ ∩ { 𝑥 ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		cotrintab.min	⊢ ( 𝜑 → ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 )
2		cotr	⊢ ( ( ∩ { 𝑥 ∣ 𝜑 } ∘ ∩ { 𝑥 ∣ 𝜑 } ) ⊆ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑢 ∀ 𝑤 ∀ 𝑣 ( ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑤 ∧ 𝑤 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ) → 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ) )
3		pm3.43	⊢ ( ( ( 𝜑 → 𝑢 𝑥 𝑤 ) ∧ ( 𝜑 → 𝑤 𝑥 𝑣 ) ) → ( 𝜑 → ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) ) )
4		cotr	⊢ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ↔ ∀ 𝑢 ∀ 𝑤 ∀ 𝑣 ( ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) → 𝑢 𝑥 𝑣 ) )
5	4	biimpi	⊢ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 → ∀ 𝑢 ∀ 𝑤 ∀ 𝑣 ( ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) → 𝑢 𝑥 𝑣 ) )
6		2sp	⊢ ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) → 𝑢 𝑥 𝑣 ) → ( ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) → 𝑢 𝑥 𝑣 ) )
7	6	sps	⊢ ( ∀ 𝑢 ∀ 𝑤 ∀ 𝑣 ( ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) → 𝑢 𝑥 𝑣 ) → ( ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) → 𝑢 𝑥 𝑣 ) )
8	1 5 7	3syl	⊢ ( 𝜑 → ( ( 𝑢 𝑥 𝑤 ∧ 𝑤 𝑥 𝑣 ) → 𝑢 𝑥 𝑣 ) )
9	3 8	sylcom	⊢ ( ( ( 𝜑 → 𝑢 𝑥 𝑤 ) ∧ ( 𝜑 → 𝑤 𝑥 𝑣 ) ) → ( 𝜑 → 𝑢 𝑥 𝑣 ) )
10	9	alanimi	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝑢 𝑥 𝑤 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 𝑥 𝑣 ) ) → ∀ 𝑥 ( 𝜑 → 𝑢 𝑥 𝑣 ) )
11		opex	⊢ ⟨ 𝑢 , 𝑤 ⟩ ∈ V
12	11	elintab	⊢ ( ⟨ 𝑢 , 𝑤 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑥 ) )
13		df-br	⊢ ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑤 ↔ ⟨ 𝑢 , 𝑤 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } )
14		df-br	⊢ ( 𝑢 𝑥 𝑤 ↔ ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑥 )
15	14	imbi2i	⊢ ( ( 𝜑 → 𝑢 𝑥 𝑤 ) ↔ ( 𝜑 → ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑥 ) )
16	15	albii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑢 𝑥 𝑤 ) ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑥 ) )
17	12 13 16	3bitr4i	⊢ ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑤 ↔ ∀ 𝑥 ( 𝜑 → 𝑢 𝑥 𝑤 ) )
18		opex	⊢ ⟨ 𝑤 , 𝑣 ⟩ ∈ V
19	18	elintab	⊢ ( ⟨ 𝑤 , 𝑣 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑥 ) )
20		df-br	⊢ ( 𝑤 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ↔ ⟨ 𝑤 , 𝑣 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } )
21		df-br	⊢ ( 𝑤 𝑥 𝑣 ↔ ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑥 )
22	21	imbi2i	⊢ ( ( 𝜑 → 𝑤 𝑥 𝑣 ) ↔ ( 𝜑 → ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑥 ) )
23	22	albii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑤 𝑥 𝑣 ) ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑥 ) )
24	19 20 23	3bitr4i	⊢ ( 𝑤 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ↔ ∀ 𝑥 ( 𝜑 → 𝑤 𝑥 𝑣 ) )
25	17 24	anbi12i	⊢ ( ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑤 ∧ 𝑤 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑢 𝑥 𝑤 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 𝑥 𝑣 ) ) )
26		opex	⊢ ⟨ 𝑢 , 𝑣 ⟩ ∈ V
27	26	elintab	⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑥 ) )
28		df-br	⊢ ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ ∩ { 𝑥 ∣ 𝜑 } )
29		df-br	⊢ ( 𝑢 𝑥 𝑣 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑥 )
30	29	imbi2i	⊢ ( ( 𝜑 → 𝑢 𝑥 𝑣 ) ↔ ( 𝜑 → ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑥 ) )
31	30	albii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑢 𝑥 𝑣 ) ↔ ∀ 𝑥 ( 𝜑 → ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑥 ) )
32	27 28 31	3bitr4i	⊢ ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ↔ ∀ 𝑥 ( 𝜑 → 𝑢 𝑥 𝑣 ) )
33	10 25 32	3imtr4i	⊢ ( ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑤 ∧ 𝑤 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ) → 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑣 )
34	33	gen2	⊢ ∀ 𝑤 ∀ 𝑣 ( ( 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑤 ∧ 𝑤 ∩ { 𝑥 ∣ 𝜑 } 𝑣 ) → 𝑢 ∩ { 𝑥 ∣ 𝜑 } 𝑣 )
35	2 34	mpgbir	⊢ ( ∩ { 𝑥 ∣ 𝜑 } ∘ ∩ { 𝑥 ∣ 𝜑 } ) ⊆ ∩ { 𝑥 ∣ 𝜑 }