cnvf1olem

		Ref	Expression
	Assertion	cnvf1olem	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ( 𝐶 ∈ ^◡ 𝐴 ∧ 𝐵 = ∪ ^◡ { 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		simprr	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → 𝐶 = ∪ ^◡ { 𝐵 } )
2		1st2nd	⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
3	2	adantrr	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
4	3	sneqd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → { 𝐵 } = { ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ } )
5	4	cnveqd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ^◡ { 𝐵 } = ^◡ { ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ } )
6	5	unieqd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ∪ ^◡ { 𝐵 } = ∪ ^◡ { ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ } )
7	1 6	eqtrd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → 𝐶 = ∪ ^◡ { ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ } )
8		opswap	⊢ ∪ ^◡ { ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ } = ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩
9	7 8	eqtrdi	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → 𝐶 = ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ )
10		simprl	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → 𝐵 ∈ 𝐴 )
11	3 10	eqeltrrd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ∈ 𝐴 )
12		fvex	⊢ ( 2^nd ‘ 𝐵 ) ∈ V
13		fvex	⊢ ( 1^st ‘ 𝐵 ) ∈ V
14	12 13	opelcnv	⊢ ( ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ ∈ ^◡ 𝐴 ↔ ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ∈ 𝐴 )
15	11 14	sylibr	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ ∈ ^◡ 𝐴 )
16	9 15	eqeltrd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → 𝐶 ∈ ^◡ 𝐴 )
17		opswap	⊢ ∪ ^◡ { ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ } = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩
18	17	eqcomi	⊢ ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ }
19	9	sneqd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → { 𝐶 } = { ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ } )
20	19	cnveqd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ^◡ { 𝐶 } = ^◡ { ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ } )
21	20	unieqd	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ∪ ^◡ { 𝐶 } = ∪ ^◡ { ⟨ ( 2^nd ‘ 𝐵 ) , ( 1^st ‘ 𝐵 ) ⟩ } )
22	18 3 21	3eqtr4a	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → 𝐵 = ∪ ^◡ { 𝐶 } )
23	16 22	jca	⊢ ( ( Rel 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ^◡ { 𝐵 } ) ) → ( 𝐶 ∈ ^◡ 𝐴 ∧ 𝐵 = ∪ ^◡ { 𝐶 } ) )

Metamath Proof Explorer

Theorem cnvf1olem

Proof