| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq2 2830 | . . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ∅)) | 
| 2 |  | raleq 3323 | . . . . . . . . . . 11
⊢ (𝑧 = ∅ → (∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦 ↔ ∀𝑥 ∈ ∅ ¬ 𝑥𝑅𝑦)) | 
| 3 | 1, 2 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑧 = ∅ → ((𝑦 ∈ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦) ↔ (𝑦 ∈ ∅ ∧ ∀𝑥 ∈ ∅ ¬ 𝑥𝑅𝑦))) | 
| 4 | 3 | rabbidva2 3438 | . . . . . . . . 9
⊢ (𝑧 = ∅ → {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑦 ∈ ∅ ∣ ∀𝑥 ∈ ∅ ¬ 𝑥𝑅𝑦}) | 
| 5 | 4 | unieqd 4920 | . . . . . . . 8
⊢ (𝑧 = ∅ → ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = ∪ {𝑦 ∈ ∅ ∣
∀𝑥 ∈ ∅
¬ 𝑥𝑅𝑦}) | 
| 6 |  | rab0 4386 | . . . . . . . . . 10
⊢ {𝑦 ∈ ∅ ∣
∀𝑥 ∈ ∅
¬ 𝑥𝑅𝑦} = ∅ | 
| 7 | 6 | unieqi 4919 | . . . . . . . . 9
⊢ ∪ {𝑦
∈ ∅ ∣ ∀𝑥 ∈ ∅ ¬ 𝑥𝑅𝑦} = ∪
∅ | 
| 8 |  | uni0 4935 | . . . . . . . . 9
⊢ ∪ ∅ = ∅ | 
| 9 | 7, 8 | eqtri 2765 | . . . . . . . 8
⊢ ∪ {𝑦
∈ ∅ ∣ ∀𝑥 ∈ ∅ ¬ 𝑥𝑅𝑦} = ∅ | 
| 10 | 5, 9 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑧 = ∅ → ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = ∅) | 
| 11 |  | 0ex 5307 | . . . . . . 7
⊢ ∅
∈ V | 
| 12 | 10, 11 | eqeltrdi 2849 | . . . . . 6
⊢ (𝑧 = ∅ → ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ V) | 
| 13 | 12 | adantl 481 | . . . . 5
⊢ ((𝑅 We V ∧ 𝑧 = ∅) → ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ V) | 
| 14 |  | ssv 4008 | . . . . . . . . . . . 12
⊢ 𝑧 ⊆ V | 
| 15 | 14 | jctl 523 | . . . . . . . . . . 11
⊢ (𝑧 ≠ ∅ → (𝑧 ⊆ V ∧ 𝑧 ≠ ∅)) | 
| 16 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑧 ∈ V | 
| 17 | 15, 16 | jctil 519 | . . . . . . . . . 10
⊢ (𝑧 ≠ ∅ → (𝑧 ∈ V ∧ (𝑧 ⊆ V ∧ 𝑧 ≠
∅))) | 
| 18 |  | 3anass 1095 | . . . . . . . . . 10
⊢ ((𝑧 ∈ V ∧ 𝑧 ⊆ V ∧ 𝑧 ≠ ∅) ↔ (𝑧 ∈ V ∧ (𝑧 ⊆ V ∧ 𝑧 ≠
∅))) | 
| 19 | 17, 18 | sylibr 234 | . . . . . . . . 9
⊢ (𝑧 ≠ ∅ → (𝑧 ∈ V ∧ 𝑧 ⊆ V ∧ 𝑧 ≠ ∅)) | 
| 20 |  | wereu 5681 | . . . . . . . . 9
⊢ ((𝑅 We V ∧ (𝑧 ∈ V ∧ 𝑧 ⊆ V ∧ 𝑧 ≠ ∅)) → ∃!𝑦 ∈ 𝑧 ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦) | 
| 21 | 19, 20 | sylan2 593 | . . . . . . . 8
⊢ ((𝑅 We V ∧ 𝑧 ≠ ∅) → ∃!𝑦 ∈ 𝑧 ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦) | 
| 22 |  | vsnid 4663 | . . . . . . . . . . . . 13
⊢ 𝑤 ∈ {𝑤} | 
| 23 |  | eleq2 2830 | . . . . . . . . . . . . 13
⊢ ({𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤} → (𝑤 ∈ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ↔ 𝑤 ∈ {𝑤})) | 
| 24 | 22, 23 | mpbiri 258 | . . . . . . . . . . . 12
⊢ ({𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤} → 𝑤 ∈ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦}) | 
| 25 |  | elrabi 3687 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} → 𝑤 ∈ 𝑧) | 
| 26 | 24, 25 | syl 17 | . . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤} → 𝑤 ∈ 𝑧) | 
| 27 |  | unieq 4918 | . . . . . . . . . . . 12
⊢ ({𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤} → ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = ∪ {𝑤}) | 
| 28 |  | unisnv 4927 | . . . . . . . . . . . 12
⊢ ∪ {𝑤}
= 𝑤 | 
| 29 | 27, 28 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤} → ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤) | 
| 30 | 26, 29 | jca 511 | . . . . . . . . . 10
⊢ ({𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤} → (𝑤 ∈ 𝑧 ∧ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤)) | 
| 31 | 30 | eximi 1835 | . . . . . . . . 9
⊢
(∃𝑤{𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤} → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤)) | 
| 32 |  | reusn 4727 | . . . . . . . . 9
⊢
(∃!𝑦 ∈
𝑧 ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦 ↔ ∃𝑤{𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = {𝑤}) | 
| 33 |  | df-rex 3071 | . . . . . . . . 9
⊢
(∃𝑤 ∈
𝑧 ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤)) | 
| 34 | 31, 32, 33 | 3imtr4i 292 | . . . . . . . 8
⊢
(∃!𝑦 ∈
𝑧 ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦 → ∃𝑤 ∈ 𝑧 ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤) | 
| 35 | 21, 34 | syl 17 | . . . . . . 7
⊢ ((𝑅 We V ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤) | 
| 36 |  | eleq1 2829 | . . . . . . . . 9
⊢ (∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤 → (∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ 𝑧 ↔ 𝑤 ∈ 𝑧)) | 
| 37 | 36 | biimparc 479 | . . . . . . . 8
⊢ ((𝑤 ∈ 𝑧 ∧ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤) → ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ 𝑧) | 
| 38 | 37 | rexlimiva 3147 | . . . . . . 7
⊢
(∃𝑤 ∈
𝑧 ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} = 𝑤 → ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ 𝑧) | 
| 39 | 35, 38 | syl 17 | . . . . . 6
⊢ ((𝑅 We V ∧ 𝑧 ≠ ∅) → ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ 𝑧) | 
| 40 | 39 | elexd 3504 | . . . . 5
⊢ ((𝑅 We V ∧ 𝑧 ≠ ∅) → ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ V) | 
| 41 | 13, 40 | pm2.61dane 3029 | . . . 4
⊢ (𝑅 We V → ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ V) | 
| 42 | 41 | ralrimivw 3150 | . . 3
⊢ (𝑅 We V → ∀𝑧 ∈ V ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ V) | 
| 43 |  | wevgblacfn.1 | . . . 4
⊢ 𝐹 = (𝑧 ∈ V ↦ ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦}) | 
| 44 | 43 | fnmpt 6708 | . . 3
⊢
(∀𝑧 ∈ V
∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ V → 𝐹 Fn V) | 
| 45 | 42, 44 | syl 17 | . 2
⊢ (𝑅 We V → 𝐹 Fn V) | 
| 46 | 43 | fvmpt2 7027 | . . . . . 6
⊢ ((𝑧 ∈ V ∧ ∪ {𝑦
∈ 𝑧 ∣
∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦} ∈ 𝑧) → (𝐹‘𝑧) = ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦}) | 
| 47 | 16, 39, 46 | sylancr 587 | . . . . 5
⊢ ((𝑅 We V ∧ 𝑧 ≠ ∅) → (𝐹‘𝑧) = ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦}) | 
| 48 | 47, 39 | eqeltrd 2841 | . . . 4
⊢ ((𝑅 We V ∧ 𝑧 ≠ ∅) → (𝐹‘𝑧) ∈ 𝑧) | 
| 49 | 48 | ex 412 | . . 3
⊢ (𝑅 We V → (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) | 
| 50 | 49 | alrimiv 1927 | . 2
⊢ (𝑅 We V → ∀𝑧(𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) | 
| 51 | 45, 50 | jca 511 | 1
⊢ (𝑅 We V → (𝐹 Fn V ∧ ∀𝑧(𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))) |