Metamath Proof Explorer

Theorem cnvcnvintabd

Description: Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020)

Ref Expression
Hypothesis cnvcnvintabd.x ⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
Assertion cnvcnvintabd ( 𝜑 → ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } )

Proof

Step Hyp Ref Expression
1 cnvcnvintabd.x ⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
2 cnvcnv ⊢ ◡ ◡ 𝑥 = ( 𝑥 ∩ ( V × V ) )
3 2 eleq2i ⊢ ( 𝑦 ∈ ◡ ◡ 𝑥 ↔ 𝑦 ∈ ( 𝑥 ∩ ( V × V ) ) )
4 elin ⊢ ( 𝑦 ∈ ( 𝑥 ∩ ( V × V ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ( V × V ) ) )
5 4 rbaib ⊢ ( 𝑦 ∈ ( V × V ) → ( 𝑦 ∈ ( 𝑥 ∩ ( V × V ) ) ↔ 𝑦 ∈ 𝑥 ) )
6 3 5 syl5bb ⊢ ( 𝑦 ∈ ( V × V ) → ( 𝑦 ∈ ◡ ◡ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
7 6 bicomd ⊢ ( 𝑦 ∈ ( V × V ) → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ◡ ◡ 𝑥 ) )
8 7 imbi2d ⊢ ( 𝑦 ∈ ( V × V ) → ( ( 𝜓 → 𝑦 ∈ 𝑥 ) ↔ ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
9 8 albidv ⊢ ( 𝑦 ∈ ( V × V ) → ( ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
10 9 pm5.32i ⊢ ( ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ) ↔ ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
11 pm5.5 ⊢ ( ∃ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ↔ 𝑦 ∈ ( V × V ) ) )
12 1 11 syl ⊢ ( 𝜑 → ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ↔ 𝑦 ∈ ( V × V ) ) )
13 12 bicomd ⊢ ( 𝜑 → ( 𝑦 ∈ ( V × V ) ↔ ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ) )
14 13 anbi1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ) )
15 10 14 syl5bb ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ) )
16 elcnvcnvintab ⊢ ( 𝑦 ∈ ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } ↔ ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ) )
17 vex ⊢ 𝑥 ∈ V
18 cnvexg ⊢ ( 𝑥 ∈ V → ◡ 𝑥 ∈ V )
19 cnvexg ⊢ ( ◡ 𝑥 ∈ V → ◡ ◡ 𝑥 ∈ V )
20 17 18 19 mp2b ⊢ ◡ ◡ 𝑥 ∈ V
21 relcnv ⊢ Rel ◡ ◡ 𝑥
22 df-rel ⊢ ( Rel ◡ ◡ 𝑥 ↔ ◡ ◡ 𝑥 ⊆ ( V × V ) )
23 21 22 mpbi ⊢ ◡ ◡ 𝑥 ⊆ ( V × V )
24 20 23 elmapintrab ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ) )
25 24 elv ⊢ ( 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
26 15 16 25 3bitr4g ⊢ ( 𝜑 → ( 𝑦 ∈ ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } ↔ 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } ) )
27 26 eqrdv ⊢ ( 𝜑 → ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } )