Proof of Theorem tz9.12lem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tz9.12lem.2 | . . . . . . . . . . 11
⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣
∈ On ∣ 𝑧 ∈
(𝑅1‘𝑣)}) | 
| 2 | 1 | funmpt2 6604 | . . . . . . . . . 10
⊢ Fun 𝐹 | 
| 3 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑦 → (𝑅1‘𝑣) =
(𝑅1‘𝑦)) | 
| 4 | 3 | eleq2d 2826 | . . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → (𝑥 ∈ (𝑅1‘𝑣) ↔ 𝑥 ∈ (𝑅1‘𝑦))) | 
| 5 | 4 | rspcev 3621 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) → ∃𝑣 ∈ On 𝑥 ∈ (𝑅1‘𝑣)) | 
| 6 |  | rabn0 4388 | . . . . . . . . . . . . 13
⊢ ({𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ On 𝑥 ∈ (𝑅1‘𝑣)) | 
| 7 | 5, 6 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) → {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)} ≠
∅) | 
| 8 |  | intex 5343 | . . . . . . . . . . . 12
⊢ ({𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ≠ ∅ ↔ ∩ {𝑣
∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ V) | 
| 9 | 7, 8 | sylib 218 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) → ∩ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ V) | 
| 10 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑥 ∈ V | 
| 11 |  | eleq1w 2823 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (𝑧 ∈ (𝑅1‘𝑣) ↔ 𝑥 ∈ (𝑅1‘𝑣))) | 
| 12 | 11 | rabbidv 3443 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)} = {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)}) | 
| 13 | 12 | inteqd 4950 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → ∩ {𝑣 ∈ On ∣ 𝑧 ∈
(𝑅1‘𝑣)} = ∩ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)}) | 
| 14 | 13 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (∩ {𝑣 ∈ On ∣ 𝑧 ∈
(𝑅1‘𝑣)} ∈ V ↔ ∩ {𝑣
∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ V)) | 
| 15 | 1 | dmmpt 6259 | . . . . . . . . . . . . 13
⊢ dom 𝐹 = {𝑧 ∈ V ∣ ∩ {𝑣
∈ On ∣ 𝑧 ∈
(𝑅1‘𝑣)} ∈ V} | 
| 16 | 14, 15 | elrab2 3694 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ dom 𝐹 ↔ (𝑥 ∈ V ∧ ∩
{𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ V)) | 
| 17 | 10, 16 | mpbiran 709 | . . . . . . . . . . 11
⊢ (𝑥 ∈ dom 𝐹 ↔ ∩ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ V) | 
| 18 | 9, 17 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) → 𝑥 ∈ dom 𝐹) | 
| 19 |  | funfvima 7251 | . . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ (𝐹 “ 𝐴))) | 
| 20 | 2, 18, 19 | sylancr 587 | . . . . . . . . 9
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ (𝐹 “ 𝐴))) | 
| 21 |  | tz9.12lem.1 | . . . . . . . . . . 11
⊢ 𝐴 ∈ V | 
| 22 | 21, 1 | tz9.12lem2 9829 | . . . . . . . . . 10
⊢ suc ∪ (𝐹
“ 𝐴) ∈
On | 
| 23 | 21, 1 | tz9.12lem1 9828 | . . . . . . . . . . . 12
⊢ (𝐹 “ 𝐴) ⊆ On | 
| 24 |  | onsucuni 7849 | . . . . . . . . . . . 12
⊢ ((𝐹 “ 𝐴) ⊆ On → (𝐹 “ 𝐴) ⊆ suc ∪
(𝐹 “ 𝐴)) | 
| 25 | 23, 24 | ax-mp 5 | . . . . . . . . . . 11
⊢ (𝐹 “ 𝐴) ⊆ suc ∪
(𝐹 “ 𝐴) | 
| 26 | 25 | sseli 3978 | . . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ (𝐹 “ 𝐴) → (𝐹‘𝑥) ∈ suc ∪
(𝐹 “ 𝐴)) | 
| 27 |  | r1ord2 9822 | . . . . . . . . . 10
⊢ (suc
∪ (𝐹 “ 𝐴) ∈ On → ((𝐹‘𝑥) ∈ suc ∪
(𝐹 “ 𝐴) →
(𝑅1‘(𝐹‘𝑥)) ⊆ (𝑅1‘suc
∪ (𝐹 “ 𝐴)))) | 
| 28 | 22, 26, 27 | mpsyl 68 | . . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ (𝐹 “ 𝐴) → (𝑅1‘(𝐹‘𝑥)) ⊆ (𝑅1‘suc
∪ (𝐹 “ 𝐴))) | 
| 29 | 20, 28 | syl6 35 | . . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) → (𝑥 ∈ 𝐴 → (𝑅1‘(𝐹‘𝑥)) ⊆ (𝑅1‘suc
∪ (𝐹 “ 𝐴)))) | 
| 30 | 29 | imp 406 | . . . . . . 7
⊢ (((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) ∧ 𝑥 ∈ 𝐴) → (𝑅1‘(𝐹‘𝑥)) ⊆ (𝑅1‘suc
∪ (𝐹 “ 𝐴))) | 
| 31 | 13, 1 | fvmptg 7013 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ V ∧ ∩ {𝑣
∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ V) → (𝐹‘𝑥) = ∩ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)}) | 
| 32 | 10, 31 | mpan 690 | . . . . . . . . . . 11
⊢ (∩ {𝑣
∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ V → (𝐹‘𝑥) = ∩ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)}) | 
| 33 | 8, 32 | sylbi 217 | . . . . . . . . . 10
⊢ ({𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ≠ ∅ → (𝐹‘𝑥) = ∩ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)}) | 
| 34 |  | ssrab2 4079 | . . . . . . . . . . 11
⊢ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ⊆ On | 
| 35 |  | onint 7811 | . . . . . . . . . . 11
⊢ (({𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ⊆ On ∧ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)} ≠ ∅) → ∩ {𝑣
∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)}) | 
| 36 | 34, 35 | mpan 690 | . . . . . . . . . 10
⊢ ({𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ≠ ∅ → ∩ {𝑣
∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)}) | 
| 37 | 33, 36 | eqeltrd 2840 | . . . . . . . . 9
⊢ ({𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} ≠ ∅ → (𝐹‘𝑥) ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)}) | 
| 38 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑥) → (𝑅1‘𝑦) =
(𝑅1‘(𝐹‘𝑥))) | 
| 39 | 38 | eleq2d 2826 | . . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑥) → (𝑥 ∈ (𝑅1‘𝑦) ↔ 𝑥 ∈ (𝑅1‘(𝐹‘𝑥)))) | 
| 40 | 4 | cbvrabv 3446 | . . . . . . . . . . 11
⊢ {𝑣 ∈ On ∣ 𝑥 ∈
(𝑅1‘𝑣)} = {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑦)} | 
| 41 | 39, 40 | elrab2 3694 | . . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)} ↔ ((𝐹‘𝑥) ∈ On ∧ 𝑥 ∈ (𝑅1‘(𝐹‘𝑥)))) | 
| 42 | 41 | simprbi 496 | . . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ {𝑣 ∈ On ∣ 𝑥 ∈ (𝑅1‘𝑣)} → 𝑥 ∈ (𝑅1‘(𝐹‘𝑥))) | 
| 43 | 7, 37, 42 | 3syl 18 | . . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) → 𝑥 ∈ (𝑅1‘(𝐹‘𝑥))) | 
| 44 | 43 | adantr 480 | . . . . . . 7
⊢ (((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (𝑅1‘(𝐹‘𝑥))) | 
| 45 | 30, 44 | sseldd 3983 | . . . . . 6
⊢ (((𝑦 ∈ On ∧ 𝑥 ∈
(𝑅1‘𝑦)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (𝑅1‘suc
∪ (𝐹 “ 𝐴))) | 
| 46 | 45 | exp31 419 | . . . . 5
⊢ (𝑦 ∈ On → (𝑥 ∈
(𝑅1‘𝑦) → (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝑅1‘suc
∪ (𝐹 “ 𝐴))))) | 
| 47 | 46 | com3r 87 | . . . 4
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ On → (𝑥 ∈ (𝑅1‘𝑦) → 𝑥 ∈ (𝑅1‘suc
∪ (𝐹 “ 𝐴))))) | 
| 48 | 47 | rexlimdv 3152 | . . 3
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → 𝑥 ∈ (𝑅1‘suc
∪ (𝐹 “ 𝐴)))) | 
| 49 | 48 | ralimia 3079 | . 2
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑅1‘suc
∪ (𝐹 “ 𝐴))) | 
| 50 |  | r1suc 9811 | . . . . 5
⊢ (suc
∪ (𝐹 “ 𝐴) ∈ On →
(𝑅1‘suc suc ∪ (𝐹 “ 𝐴)) = 𝒫
(𝑅1‘suc ∪ (𝐹 “ 𝐴))) | 
| 51 | 22, 50 | ax-mp 5 | . . . 4
⊢
(𝑅1‘suc suc ∪ (𝐹 “ 𝐴)) = 𝒫
(𝑅1‘suc ∪ (𝐹 “ 𝐴)) | 
| 52 | 51 | eleq2i 2832 | . . 3
⊢ (𝐴 ∈
(𝑅1‘suc suc ∪ (𝐹 “ 𝐴)) ↔ 𝐴 ∈ 𝒫
(𝑅1‘suc ∪ (𝐹 “ 𝐴))) | 
| 53 | 21 | elpw 4603 | . . 3
⊢ (𝐴 ∈ 𝒫
(𝑅1‘suc ∪ (𝐹 “ 𝐴)) ↔ 𝐴 ⊆ (𝑅1‘suc
∪ (𝐹 “ 𝐴))) | 
| 54 |  | dfss3 3971 | . . 3
⊢ (𝐴 ⊆
(𝑅1‘suc ∪ (𝐹 “ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑅1‘suc
∪ (𝐹 “ 𝐴))) | 
| 55 | 52, 53, 54 | 3bitri 297 | . 2
⊢ (𝐴 ∈
(𝑅1‘suc suc ∪ (𝐹 “ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑅1‘suc
∪ (𝐹 “ 𝐴))) | 
| 56 | 49, 55 | sylibr 234 | 1
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → 𝐴 ∈ (𝑅1‘suc suc
∪ (𝐹 “ 𝐴))) |