| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3anrot 1100 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) | 
| 2 |  | ordtval.1 | . . . . . . . . . . . . . 14
⊢ 𝑋 = dom 𝑅 | 
| 3 | 2 | tsrlemax 18631 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ TosetRel ∧ (𝑦 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎 ∨ 𝑦𝑅𝑏))) | 
| 4 | 1, 3 | sylan2br 595 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎 ∨ 𝑦𝑅𝑏))) | 
| 5 | 4 | 3exp2 1355 | . . . . . . . . . . 11
⊢ (𝑅 ∈ TosetRel → (𝑎 ∈ 𝑋 → (𝑏 ∈ 𝑋 → (𝑦 ∈ 𝑋 → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎 ∨ 𝑦𝑅𝑏)))))) | 
| 6 | 5 | imp42 426 | . . . . . . . . . 10
⊢ (((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎 ∨ 𝑦𝑅𝑏))) | 
| 7 | 6 | notbid 318 | . . . . . . . . 9
⊢ (((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ ¬ (𝑦𝑅𝑎 ∨ 𝑦𝑅𝑏))) | 
| 8 |  | ioran 986 | . . . . . . . . 9
⊢ (¬
(𝑦𝑅𝑎 ∨ 𝑦𝑅𝑏) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)) | 
| 9 | 7, 8 | bitrdi 287 | . . . . . . . 8
⊢ (((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏))) | 
| 10 | 9 | rabbidva 3443 | . . . . . . 7
⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)}) | 
| 11 |  | ifcl 4571 | . . . . . . . . 9
⊢ ((𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋) | 
| 12 | 11 | ancoms 458 | . . . . . . . 8
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋) | 
| 13 |  | dmexg 7923 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ TosetRel → dom
𝑅 ∈
V) | 
| 14 | 2, 13 | eqeltrid 2845 | . . . . . . . . . . 11
⊢ (𝑅 ∈ TosetRel → 𝑋 ∈ V) | 
| 15 | 14 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑋 ∈ V) | 
| 16 |  | rabexg 5337 | . . . . . . . . . 10
⊢ (𝑋 ∈ V → {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V) | 
| 17 | 15, 16 | syl 17 | . . . . . . . . 9
⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V) | 
| 18 | 10, 17 | eqeltrd 2841 | . . . . . . . 8
⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) | 
| 19 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) | 
| 20 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (𝑦𝑅𝑥 ↔ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎))) | 
| 21 | 20 | notbid 318 | . . . . . . . . . . 11
⊢ (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎))) | 
| 22 | 21 | rabbidv 3444 | . . . . . . . . . 10
⊢ (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)}) | 
| 23 | 19, 22 | elrnmpt1s 5970 | . . . . . . . . 9
⊢
((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})) | 
| 24 |  | ordtval.2 | . . . . . . . . 9
⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) | 
| 25 | 23, 24 | eleqtrrdi 2852 | . . . . . . . 8
⊢
((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴) | 
| 26 | 12, 18, 25 | syl2an2 686 | . . . . . . 7
⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴) | 
| 27 | 10, 26 | eqeltrrd 2842 | . . . . . 6
⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴) | 
| 28 | 27 | ralrimivva 3202 | . . . . 5
⊢ (𝑅 ∈ TosetRel →
∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴) | 
| 29 |  | rabexg 5337 | . . . . . . . 8
⊢ (𝑋 ∈ V → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V) | 
| 30 | 14, 29 | syl 17 | . . . . . . 7
⊢ (𝑅 ∈ TosetRel → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V) | 
| 31 | 30 | ralrimivw 3150 | . . . . . 6
⊢ (𝑅 ∈ TosetRel →
∀𝑎 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V) | 
| 32 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑎)) | 
| 33 | 32 | notbid 318 | . . . . . . . . 9
⊢ (𝑥 = 𝑎 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑎)) | 
| 34 | 33 | rabbidv 3444 | . . . . . . . 8
⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎}) | 
| 35 | 34 | cbvmptv 5255 | . . . . . . 7
⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑎 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎}) | 
| 36 |  | ineq1 4213 | . . . . . . . . . 10
⊢ (𝑧 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) = ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏})) | 
| 37 |  | inrab 4316 | . . . . . . . . . 10
⊢ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} | 
| 38 | 36, 37 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝑧 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)}) | 
| 39 | 38 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑧 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} → ((𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)) | 
| 40 | 39 | ralbidv 3178 | . . . . . . 7
⊢ (𝑧 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} → (∀𝑏 ∈ 𝑋 (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑏 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)) | 
| 41 | 35, 40 | ralrnmptw 7114 | . . . . . 6
⊢
(∀𝑎 ∈
𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏 ∈ 𝑋 (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)) | 
| 42 | 31, 41 | syl 17 | . . . . 5
⊢ (𝑅 ∈ TosetRel →
(∀𝑧 ∈ ran
(𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏 ∈ 𝑋 (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)) | 
| 43 | 28, 42 | mpbird 257 | . . . 4
⊢ (𝑅 ∈ TosetRel →
∀𝑧 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏 ∈ 𝑋 (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴) | 
| 44 |  | rabexg 5337 | . . . . . . . 8
⊢ (𝑋 ∈ V → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V) | 
| 45 | 14, 44 | syl 17 | . . . . . . 7
⊢ (𝑅 ∈ TosetRel → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V) | 
| 46 | 45 | ralrimivw 3150 | . . . . . 6
⊢ (𝑅 ∈ TosetRel →
∀𝑏 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V) | 
| 47 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑏)) | 
| 48 | 47 | notbid 318 | . . . . . . . . 9
⊢ (𝑥 = 𝑏 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑏)) | 
| 49 | 48 | rabbidv 3444 | . . . . . . . 8
⊢ (𝑥 = 𝑏 → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) | 
| 50 | 49 | cbvmptv 5255 | . . . . . . 7
⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) | 
| 51 |  | ineq2 4214 | . . . . . . . 8
⊢ (𝑤 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏} → (𝑧 ∩ 𝑤) = (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏})) | 
| 52 | 51 | eleq1d 2826 | . . . . . . 7
⊢ (𝑤 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏} → ((𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)) | 
| 53 | 50, 52 | ralrnmptw 7114 | . . . . . 6
⊢
(∀𝑏 ∈
𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V → (∀𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧 ∩ 𝑤) ∈ 𝐴 ↔ ∀𝑏 ∈ 𝑋 (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)) | 
| 54 | 46, 53 | syl 17 | . . . . 5
⊢ (𝑅 ∈ TosetRel →
(∀𝑤 ∈ ran
(𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧 ∩ 𝑤) ∈ 𝐴 ↔ ∀𝑏 ∈ 𝑋 (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)) | 
| 55 | 54 | ralbidv 3178 | . . . 4
⊢ (𝑅 ∈ TosetRel →
(∀𝑧 ∈ ran
(𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧 ∩ 𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏 ∈ 𝑋 (𝑧 ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)) | 
| 56 | 43, 55 | mpbird 257 | . . 3
⊢ (𝑅 ∈ TosetRel →
∀𝑧 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧 ∩ 𝑤) ∈ 𝐴) | 
| 57 | 24 | raleqi 3324 | . . . 4
⊢
(∀𝑤 ∈
𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 ↔ ∀𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧 ∩ 𝑤) ∈ 𝐴) | 
| 58 | 24, 57 | raleqbii 3344 | . . 3
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧 ∩ 𝑤) ∈ 𝐴) | 
| 59 | 56, 58 | sylibr 234 | . 2
⊢ (𝑅 ∈ TosetRel →
∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) | 
| 60 | 14 | pwexd 5379 | . . . 4
⊢ (𝑅 ∈ TosetRel →
𝒫 𝑋 ∈
V) | 
| 61 |  | ssrab2 4080 | . . . . . . . 8
⊢ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋 | 
| 62 | 14 | adantr 480 | . . . . . . . . 9
⊢ ((𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V) | 
| 63 |  | elpw2g 5333 | . . . . . . . . 9
⊢ (𝑋 ∈ V → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋)) | 
| 64 | 62, 63 | syl 17 | . . . . . . . 8
⊢ ((𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋)) | 
| 65 | 61, 64 | mpbiri 258 | . . . . . . 7
⊢ ((𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋) | 
| 66 | 65 | fmpttd 7135 | . . . . . 6
⊢ (𝑅 ∈ TosetRel → (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋) | 
| 67 | 66 | frnd 6744 | . . . . 5
⊢ (𝑅 ∈ TosetRel → ran
(𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋) | 
| 68 | 24, 67 | eqsstrid 4022 | . . . 4
⊢ (𝑅 ∈ TosetRel → 𝐴 ⊆ 𝒫 𝑋) | 
| 69 | 60, 68 | ssexd 5324 | . . 3
⊢ (𝑅 ∈ TosetRel → 𝐴 ∈ V) | 
| 70 |  | inficl 9465 | . . 3
⊢ (𝐴 ∈ V → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴)) | 
| 71 | 69, 70 | syl 17 | . 2
⊢ (𝑅 ∈ TosetRel →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴)) | 
| 72 | 59, 71 | mpbid 232 | 1
⊢ (𝑅 ∈ TosetRel →
(fi‘𝐴) = 𝐴) |