cnviin

Description: The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012)

		Ref	Expression
	Assertion	cnviin	⊢ ( 𝐴 ≠ ∅ → ^◡ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ^◡ ∩ 𝑥 ∈ 𝐴 𝐵
2		relcnv	⊢ Rel ^◡ 𝐵
3		df-rel	⊢ ( Rel ^◡ 𝐵 ↔ ^◡ 𝐵 ⊆ ( V × V ) )
4	2 3	mpbi	⊢ ^◡ 𝐵 ⊆ ( V × V )
5	4	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V )
6		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V ) ) → ∃ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V ) )
7	5 6	mpan2	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V ) )
8		iinss	⊢ ( ∃ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V ) → ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V ) )
9	7 8	syl	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V ) )
10		df-rel	⊢ ( Rel ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ↔ ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ⊆ ( V × V ) )
11	9 10	sylibr	⊢ ( 𝐴 ≠ ∅ → Rel ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 )
12		opex	⊢ ⟨ 𝑏 , 𝑎 ⟩ ∈ V
13		eliin	⊢ ( ⟨ 𝑏 , 𝑎 ⟩ ∈ V → ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑏 , 𝑎 ⟩ ∈ 𝐵 ) )
14	12 13	ax-mp	⊢ ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑏 , 𝑎 ⟩ ∈ 𝐵 )
15		vex	⊢ 𝑎 ∈ V
16		vex	⊢ 𝑏 ∈ V
17	15 16	opelcnv	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ^◡ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ⟨ 𝑏 , 𝑎 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝐵 )
18		opex	⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
19		eliin	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ V → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑎 , 𝑏 ⟩ ∈ ^◡ 𝐵 ) )
20	18 19	ax-mp	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑎 , 𝑏 ⟩ ∈ ^◡ 𝐵 )
21	15 16	opelcnv	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ^◡ 𝐵 ↔ ⟨ 𝑏 , 𝑎 ⟩ ∈ 𝐵 )
22	21	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑎 , 𝑏 ⟩ ∈ ^◡ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑏 , 𝑎 ⟩ ∈ 𝐵 )
23	20 22	bitri	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑏 , 𝑎 ⟩ ∈ 𝐵 )
24	14 17 23	3bitr4i	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ^◡ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 )
25	24	eqrelriv	⊢ ( ( Rel ^◡ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ Rel ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 ) → ^◡ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 )
26	1 11 25	sylancr	⊢ ( 𝐴 ≠ ∅ → ^◡ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ^◡ 𝐵 )

Metamath Proof Explorer

Theorem cnviin

Proof