| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | breq2 5146 | . . . . . . . 8
⊢ (𝑡 = 𝑠 → (𝑥𝑅𝑡 ↔ 𝑥𝑅𝑠)) | 
| 2 | 1 | cbvexvw 2035 | . . . . . . 7
⊢
(∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠) | 
| 3 |  | breq2 5146 | . . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑍 → (𝑥𝑅𝑠 ↔ 𝑥𝑅𝑍)) | 
| 4 | 3 | anbi1d 631 | . . . . . . . . . . . . 13
⊢ (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)))) | 
| 5 |  | bianir 1058 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ≠ 𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → 𝑥𝑅𝑡) | 
| 6 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑡 ∈ V | 
| 7 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑡 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑡)) | 
| 8 |  | neeq1 3002 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑡 → (𝑦 ≠ 𝑍 ↔ 𝑡 ≠ 𝑍)) | 
| 9 | 7, 8 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑡 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑡 ∧ 𝑡 ≠ 𝑍))) | 
| 10 | 6, 9 | spcev 3605 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥𝑅𝑡 ∧ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)) | 
| 11 | 10 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑅𝑡 → (𝑡 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 12 | 5, 11 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ≠ 𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (𝑡 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 13 | 12 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 ≠ 𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑡 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))) | 
| 14 | 13 | pm2.43a 54 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ≠ 𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 15 | 14 | adantld 490 | . . . . . . . . . . . . . 14
⊢ (𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 16 |  | nne 2943 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑡 ≠ 𝑍 ↔ 𝑡 = 𝑍) | 
| 17 |  | notbi 319 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) | 
| 18 |  | bianir 1058 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((¬
𝑡 ≠ 𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) → ¬ 𝑥𝑅𝑡) | 
| 19 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑍 = 𝑡 → (𝑥𝑅𝑍 ↔ 𝑥𝑅𝑡)) | 
| 20 | 19 | eqcoms 2744 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑍 → (𝑥𝑅𝑍 ↔ 𝑥𝑅𝑡)) | 
| 21 |  | pm2.24 124 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥𝑅𝑡 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 22 | 20, 21 | biimtrdi 253 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑍 → (𝑥𝑅𝑍 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))) | 
| 23 | 22 | com13 88 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑥𝑅𝑡 → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))) | 
| 24 | 18, 23 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
𝑡 ≠ 𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))) | 
| 25 | 24 | ex 412 | . . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑡 ≠ 𝑍 → ((¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))) | 
| 26 | 17, 25 | biimtrid 242 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑡 ≠ 𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))) | 
| 27 | 26 | com13 88 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑅𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (¬ 𝑡 ≠ 𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))) | 
| 28 | 27 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (¬ 𝑡 ≠ 𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))) | 
| 29 | 28 | com13 88 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑍 → (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))) | 
| 30 | 16, 29 | sylbi 217 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑡 ≠ 𝑍 → (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))) | 
| 31 | 30 | pm2.43i 52 | . . . . . . . . . . . . . 14
⊢ (¬
𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 32 | 15, 31 | pm2.61i 182 | . . . . . . . . . . . . 13
⊢ ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)) | 
| 33 | 4, 32 | biimtrdi 253 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 34 |  | vex 3483 | . . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V | 
| 35 |  | breq2 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑠 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑠)) | 
| 36 |  | neeq1 3002 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑠 → (𝑦 ≠ 𝑍 ↔ 𝑠 ≠ 𝑍)) | 
| 37 | 35, 36 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑠 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍))) | 
| 38 | 34, 37 | spcev 3605 | . . . . . . . . . . . . . . 15
⊢ ((𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)) | 
| 39 | 38 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝑥𝑅𝑠 → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 41 | 40 | com12 32 | . . . . . . . . . . . 12
⊢ (𝑠 ≠ 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 42 | 33, 41 | pm2.61ine 3024 | . . . . . . . . . . 11
⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)) | 
| 43 | 42 | expcom 413 | . . . . . . . . . 10
⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 44 | 43 | exlimiv 1929 | . . . . . . . . 9
⊢
(∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 45 | 44 | com12 32 | . . . . . . . 8
⊢ (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 46 | 45 | exlimiv 1929 | . . . . . . 7
⊢
(∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 47 | 2, 46 | sylbi 217 | . . . . . 6
⊢
(∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 48 | 47 | imp 406 | . . . . 5
⊢
((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)) | 
| 49 | 48 | a1i 11 | . . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))) | 
| 50 | 49 | ss2abdv 4065 | . . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)}) | 
| 51 |  | suppvalbr 8190 | . . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))}) | 
| 52 |  | cnvimadfsn 8198 | . . . 4
⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)} | 
| 53 | 52 | a1i 11 | . . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)}) | 
| 54 | 50, 51, 53 | 3sstr4d 4038 | . 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) ⊆ (◡𝑅 “ (V ∖ {𝑍}))) | 
| 55 |  | suppimacnvss 8199 | . 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍)) | 
| 56 | 54, 55 | eqssd 4000 | 1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍}))) |