Theorem cnvtrucl0

Description: The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

	Ref	Expression
Assertion	cnvtrucl0	⊢ ( 𝑋 ∈ 𝑉 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ⊤ ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ ⊤ ) } )

Proof

Step	Hyp	Ref	Expression
1		idd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ( ⊤ → ⊤ ) )
2		idd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = ◡ 𝑥 ) → ( ⊤ → ⊤ ) )
3		biidd	⊢ ( 𝑥 = 𝑋 → ( ⊤ ↔ ⊤ ) )
4		ssidd	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑋 )
5		elex	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
6		trud	⊢ ( 𝑋 ∈ 𝑉 → ⊤ )
7	1 2 3 4 5 6	clcnvlem	⊢ ( 𝑋 ∈ 𝑉 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ⊤ ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ ⊤ ) } )