Proof of Theorem aomclem6
| Step | Hyp | Ref
| Expression |
| 1 | | ssid 4006 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
| 2 | | aomclem6.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ On) |
| 3 | 2 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝐴 ∈ On) |
| 4 | | sseq1 4009 |
. . . . . 6
⊢ (𝑐 = 𝑑 → (𝑐 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴)) |
| 5 | 4 | anbi2d 630 |
. . . . 5
⊢ (𝑐 = 𝑑 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑑 ⊆ 𝐴))) |
| 6 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = 𝑑 → (𝐻‘𝑐) = (𝐻‘𝑑)) |
| 7 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = 𝑑 → (𝑅1‘𝑐) =
(𝑅1‘𝑑)) |
| 8 | 6, 7 | weeq12d 5674 |
. . . . 5
⊢ (𝑐 = 𝑑 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝑑) We (𝑅1‘𝑑))) |
| 9 | 5, 8 | imbi12d 344 |
. . . 4
⊢ (𝑐 = 𝑑 → (((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)) ↔ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)))) |
| 10 | | sseq1 4009 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (𝑐 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
| 11 | 10 | anbi2d 630 |
. . . . 5
⊢ (𝑐 = 𝐴 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴))) |
| 12 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (𝐻‘𝑐) = (𝐻‘𝐴)) |
| 13 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (𝑅1‘𝑐) =
(𝑅1‘𝐴)) |
| 14 | 12, 13 | weeq12d 5674 |
. . . . 5
⊢ (𝑐 = 𝐴 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝐴) We (𝑅1‘𝐴))) |
| 15 | 11, 14 | imbi12d 344 |
. . . 4
⊢ (𝑐 = 𝐴 → (((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)) ↔ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴)))) |
| 16 | | aomclem6.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} |
| 17 | | aomclem6.c |
. . . . . . . . . . . . . 14
⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵)) |
| 18 | | aomclem6.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom
𝑧) ∖ ran 𝑎)))) |
| 19 | | aomclem6.e |
. . . . . . . . . . . . . 14
⊢ 𝐸 = {〈𝑎, 𝑏〉 ∣ ∩
(◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})} |
| 20 | | aomclem6.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} |
| 21 | | aomclem6.g |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) |
| 22 | | dmeq 5914 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐻 ↾ 𝑐) → dom 𝑧 = dom (𝐻 ↾ 𝑐)) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = dom (𝐻 ↾ 𝑐)) |
| 24 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ∈ On) |
| 25 | | onss 7805 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ On → 𝑐 ⊆ On) |
| 26 | | aomclem6.h |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺)) |
| 27 | 26 | tfr1 8437 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 Fn On |
| 28 | | fnssres 6691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻 ↾ 𝑐) Fn 𝑐) |
| 29 | 27, 28 | mpan 690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ⊆ On → (𝐻 ↾ 𝑐) Fn 𝑐) |
| 30 | | fndm 6671 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ↾ 𝑐) Fn 𝑐 → dom (𝐻 ↾ 𝑐) = 𝑐) |
| 31 | 24, 25, 29, 30 | 4syl 19 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom (𝐻 ↾ 𝑐) = 𝑐) |
| 32 | 23, 31 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = 𝑐) |
| 33 | 32, 24 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ∈ On) |
| 34 | 32 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 ↔ 𝑎 ∈ 𝑐)) |
| 35 | 34 | biimpa 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ∈ 𝑐) |
| 36 | | simpll2 1214 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) |
| 37 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝜑) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝜑) |
| 39 | | onelss 6426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (dom
𝑧 ∈ On → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧)) |
| 40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧)) |
| 41 | 40 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ dom 𝑧) |
| 42 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ⊆ 𝐴) |
| 43 | 32, 42 | eqsstrd 4018 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ⊆ 𝐴) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧 ⊆ 𝐴) |
| 45 | 41, 44 | sstrd 3994 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ 𝐴) |
| 46 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑎 → (𝑑 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴)) |
| 47 | 46 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → ((𝜑 ∧ 𝑑 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑎 ⊆ 𝐴))) |
| 48 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑎 → (𝐻‘𝑑) = (𝐻‘𝑎)) |
| 49 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑎 → (𝑅1‘𝑑) =
(𝑅1‘𝑎)) |
| 50 | 48, 49 | weeq12d 5674 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → ((𝐻‘𝑑) We (𝑅1‘𝑑) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎))) |
| 51 | 47, 50 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = 𝑎 → (((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ↔ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎)))) |
| 52 | 51 | rspcva 3620 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) → ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎))) |
| 53 | 52 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) ∧ (𝜑 ∧ 𝑎 ⊆ 𝐴)) → (𝐻‘𝑎) We (𝑅1‘𝑎)) |
| 54 | 35, 36, 38, 45, 53 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝐻‘𝑎) We (𝑅1‘𝑎)) |
| 55 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎)) |
| 56 | 55 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎)) |
| 57 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝑐 → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎)) |
| 58 | 35, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎)) |
| 59 | 56, 58 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = (𝐻‘𝑎)) |
| 60 | | weeq1 5672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧‘𝑎) = (𝐻‘𝑎) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎))) |
| 61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎))) |
| 62 | 54, 61 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) We (𝑅1‘𝑎)) |
| 63 | 62 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) |
| 64 | 37, 2 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐴 ∈ On) |
| 65 | | aomclem6.y |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑎 ∈ 𝒫
(𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖
{∅}))) |
| 66 | 37, 65 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → ∀𝑎 ∈ 𝒫
(𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖
{∅}))) |
| 67 | 16, 17, 18, 19, 20, 21, 33, 63, 64, 43, 66 | aomclem5 43070 |
. . . . . . . . . . . . 13
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘dom 𝑧)) |
| 68 | 32 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑅1‘dom
𝑧) =
(𝑅1‘𝑐)) |
| 69 | | weeq2 5673 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘dom 𝑧) = (𝑅1‘𝑐) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1‘𝑐))) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝐺 We (𝑅1‘dom 𝑧) ↔ 𝐺 We (𝑅1‘𝑐))) |
| 71 | 67, 70 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘𝑐)) |
| 72 | 71 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐))) |
| 73 | 72 | alrimiv 1927 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐))) |
| 74 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) |
| 75 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧 𝑑 = (𝐻 ↾ 𝑐) |
| 76 | | nfsbc1v 3808 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧[𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) |
| 77 | 75, 76 | nfim 1896 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) |
| 78 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑑 → (𝑧 = (𝐻 ↾ 𝑐) ↔ 𝑑 = (𝐻 ↾ 𝑐))) |
| 79 | | sbceq1a 3799 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑑 → (𝐺 We (𝑅1‘𝑐) ↔ [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
| 80 | 78, 79 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑑 → ((𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ (𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))) |
| 81 | 74, 77, 80 | cbvalv1 2343 |
. . . . . . . . . 10
⊢
(∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
| 82 | 73, 81 | sylib 218 |
. . . . . . . . 9
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
| 83 | | nfsbc1v 3808 |
. . . . . . . . . 10
⊢
Ⅎ𝑑[(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) |
| 84 | | fnfun 6668 |
. . . . . . . . . . . 12
⊢ (𝐻 Fn On → Fun 𝐻) |
| 85 | 27, 84 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun 𝐻 |
| 86 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑐 ∈ V |
| 87 | | resfunexg 7235 |
. . . . . . . . . . 11
⊢ ((Fun
𝐻 ∧ 𝑐 ∈ V) → (𝐻 ↾ 𝑐) ∈ V) |
| 88 | 85, 86, 87 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐻 ↾ 𝑐) ∈ V |
| 89 | | sbceq1a 3799 |
. . . . . . . . . 10
⊢ (𝑑 = (𝐻 ↾ 𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
| 90 | 83, 88, 89 | ceqsal 3519 |
. . . . . . . . 9
⊢
(∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) |
| 91 | 82, 90 | sylib 218 |
. . . . . . . 8
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) |
| 92 | | sbccow 3811 |
. . . . . . . 8
⊢
([(𝐻 ↾
𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐)) |
| 93 | 91, 92 | sylib 218 |
. . . . . . 7
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐)) |
| 94 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 |
| 95 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑅1‘𝑐) |
| 96 | 94, 95 | nfwe 5660 |
. . . . . . . . 9
⊢
Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐) |
| 97 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺) |
| 98 | | weeq1 5672 |
. . . . . . . . . 10
⊢ (𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
| 99 | 97, 98 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
| 100 | 96, 99 | sbciegf 3827 |
. . . . . . . 8
⊢ ((𝐻 ↾ 𝑐) ∈ V → ([(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
| 101 | 88, 100 | ax-mp 5 |
. . . . . . 7
⊢
([(𝐻 ↾
𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)) |
| 102 | 93, 101 | sylib 218 |
. . . . . 6
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)) |
| 103 | | recsval 8444 |
. . . . . . . . 9
⊢ (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))) |
| 104 | 26 | fveq1i 6907 |
. . . . . . . . 9
⊢ (𝐻‘𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) |
| 105 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(𝑅1‘dom 𝑧) ∈ V |
| 106 | 105, 105 | xpex 7773 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘dom 𝑧) × (𝑅1‘dom
𝑧)) ∈
V |
| 107 | 106 | inex2 5318 |
. . . . . . . . . . . . 13
⊢ (if(dom
𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) ∈ V |
| 108 | 21, 107 | eqeltri 2837 |
. . . . . . . . . . . 12
⊢ 𝐺 ∈ V |
| 109 | 108 | csbex 5311 |
. . . . . . . . . . 11
⊢
⦋(𝐻
↾ 𝑐) / 𝑧⦌𝐺 ∈ V |
| 110 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺) |
| 111 | 110 | fvmpts 7019 |
. . . . . . . . . . 11
⊢ (((𝐻 ↾ 𝑐) ∈ V ∧ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺) |
| 112 | 88, 109, 111 | mp2an 692 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 |
| 113 | 26 | reseq1i 5993 |
. . . . . . . . . . 11
⊢ (𝐻 ↾ 𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐) |
| 114 | 113 | fveq2i 6909 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)) |
| 115 | 112, 114 | eqtr3i 2767 |
. . . . . . . . 9
⊢
⦋(𝐻
↾ 𝑐) / 𝑧⦌𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)) |
| 116 | 103, 104,
115 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (𝑐 ∈ On → (𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺) |
| 117 | | weeq1 5672 |
. . . . . . . 8
⊢ ((𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
| 118 | 116, 117 | syl 17 |
. . . . . . 7
⊢ (𝑐 ∈ On → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
| 119 | 118 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
| 120 | 102, 119 | mpbird 257 |
. . . . 5
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝐻‘𝑐) We (𝑅1‘𝑐)) |
| 121 | 120 | 3exp 1120 |
. . . 4
⊢ (𝑐 ∈ On → (∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) → ((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)))) |
| 122 | 9, 15, 121 | tfis3 7879 |
. . 3
⊢ (𝐴 ∈ On → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴))) |
| 123 | 3, 122 | mpcom 38 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴)) |
| 124 | 1, 123 | mpan2 691 |
1
⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴)) |