Proof of Theorem aomclem6
Step | Hyp | Ref
| Expression |
1 | | ssid 3923 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
2 | | aomclem6.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ On) |
3 | 2 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝐴 ∈ On) |
4 | | sseq1 3926 |
. . . . . 6
⊢ (𝑐 = 𝑑 → (𝑐 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴)) |
5 | 4 | anbi2d 632 |
. . . . 5
⊢ (𝑐 = 𝑑 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑑 ⊆ 𝐴))) |
6 | | fveq2 6717 |
. . . . . 6
⊢ (𝑐 = 𝑑 → (𝐻‘𝑐) = (𝐻‘𝑑)) |
7 | | fveq2 6717 |
. . . . . 6
⊢ (𝑐 = 𝑑 → (𝑅1‘𝑐) =
(𝑅1‘𝑑)) |
8 | 6, 7 | weeq12d 40568 |
. . . . 5
⊢ (𝑐 = 𝑑 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝑑) We (𝑅1‘𝑑))) |
9 | 5, 8 | imbi12d 348 |
. . . 4
⊢ (𝑐 = 𝑑 → (((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)) ↔ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)))) |
10 | | sseq1 3926 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (𝑐 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
11 | 10 | anbi2d 632 |
. . . . 5
⊢ (𝑐 = 𝐴 → ((𝜑 ∧ 𝑐 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴))) |
12 | | fveq2 6717 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (𝐻‘𝑐) = (𝐻‘𝐴)) |
13 | | fveq2 6717 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (𝑅1‘𝑐) =
(𝑅1‘𝐴)) |
14 | 12, 13 | weeq12d 40568 |
. . . . 5
⊢ (𝑐 = 𝐴 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ (𝐻‘𝐴) We (𝑅1‘𝐴))) |
15 | 11, 14 | imbi12d 348 |
. . . 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 5772 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐻 ↾ 𝑐) → dom 𝑧 = dom (𝐻 ↾ 𝑐)) |
23 | 22 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 = dom (𝐻 ↾ 𝑐)) |
24 | | simpl1 1193 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ∈ On) |
25 | | onss 7568 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ On → 𝑐 ⊆ On) |
26 | | aomclem6.h |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺)) |
27 | 26 | tfr1 8133 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 Fn On |
28 | | fnssres 6500 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻 Fn On ∧ 𝑐 ⊆ On) → (𝐻 ↾ 𝑐) Fn 𝑐) |
29 | 27, 28 | mpan 690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ⊆ On → (𝐻 ↾ 𝑐) Fn 𝑐) |
30 | | fndm 6481 |
. . . . . . . . . . . . . . . . 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 2838 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ∈ On) |
34 | 32 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 ↔ 𝑎 ∈ 𝑐)) |
35 | 34 | biimpa 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ∈ 𝑐) |
36 | | simpll2 1215 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) |
37 | | simpl3l 1230 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝜑) |
38 | 37 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝜑) |
39 | | onelss 6255 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (dom
𝑧 ∈ On → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧)) |
40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑎 ∈ dom 𝑧 → 𝑎 ⊆ dom 𝑧)) |
41 | 40 | imp 410 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ dom 𝑧) |
42 | | simpl3r 1231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝑐 ⊆ 𝐴) |
43 | 32, 42 | eqsstrd 3939 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → dom 𝑧 ⊆ 𝐴) |
44 | 43 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → dom 𝑧 ⊆ 𝐴) |
45 | 41, 44 | sstrd 3911 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → 𝑎 ⊆ 𝐴) |
46 | | sseq1 3926 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑎 → (𝑑 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴)) |
47 | 46 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → ((𝜑 ∧ 𝑑 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑎 ⊆ 𝐴))) |
48 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑎 → (𝐻‘𝑑) = (𝐻‘𝑎)) |
49 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑎 → (𝑅1‘𝑑) =
(𝑅1‘𝑎)) |
50 | 48, 49 | weeq12d 40568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → ((𝐻‘𝑑) We (𝑅1‘𝑑) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎))) |
51 | 47, 50 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = 𝑎 → (((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ↔ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎)))) |
52 | 51 | rspcva 3535 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) → ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝐻‘𝑎) We (𝑅1‘𝑎))) |
53 | 52 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝑐 ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑))) ∧ (𝜑 ∧ 𝑎 ⊆ 𝐴)) → (𝐻‘𝑎) We (𝑅1‘𝑎)) |
54 | 35, 36, 38, 45, 53 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝐻‘𝑎) We (𝑅1‘𝑎)) |
55 | | fveq1 6716 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎)) |
56 | 55 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = ((𝐻 ↾ 𝑐)‘𝑎)) |
57 | | fvres 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝑐 → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎)) |
58 | 35, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝐻 ↾ 𝑐)‘𝑎) = (𝐻‘𝑎)) |
59 | 56, 58 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) = (𝐻‘𝑎)) |
60 | | weeq1 5539 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧‘𝑎) = (𝐻‘𝑎) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝐻‘𝑎) We (𝑅1‘𝑎))) |
62 | 54, 61 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) ∧ 𝑎 ∈ dom 𝑧) → (𝑧‘𝑎) We (𝑅1‘𝑎)) |
63 | 62 | ralrimiva 3105 |
. . . . . . . . . . . . . 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 40586 |
. . . . . . . . . . . . 13
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘dom 𝑧)) |
68 | 32 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → (𝑅1‘dom
𝑧) =
(𝑅1‘𝑐)) |
69 | | weeq2 5540 |
. . . . . . . . . . . . . 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 235 |
. . . . . . . . . . . 12
⊢ (((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) ∧ 𝑧 = (𝐻 ↾ 𝑐)) → 𝐺 We (𝑅1‘𝑐)) |
72 | 71 | ex 416 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐))) |
73 | 72 | alrimiv 1935 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐))) |
74 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) |
75 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧 𝑑 = (𝐻 ↾ 𝑐) |
76 | | nfsbc1v 3714 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧[𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) |
77 | 75, 76 | nfim 1904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) |
78 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑑 → (𝑧 = (𝐻 ↾ 𝑐) ↔ 𝑑 = (𝐻 ↾ 𝑐))) |
79 | | sbceq1a 3705 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑑 → (𝐺 We (𝑅1‘𝑐) ↔ [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
80 | 78, 79 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑑 → ((𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ (𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)))) |
81 | 74, 77, 80 | cbvalv1 2341 |
. . . . . . . . . 10
⊢
(∀𝑧(𝑧 = (𝐻 ↾ 𝑐) → 𝐺 We (𝑅1‘𝑐)) ↔ ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
82 | 73, 81 | sylib 221 |
. . . . . . . . 9
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
83 | | nfsbc1v 3714 |
. . . . . . . . . 10
⊢
Ⅎ𝑑[(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) |
84 | | fnfun 6479 |
. . . . . . . . . . . 12
⊢ (𝐻 Fn On → Fun 𝐻) |
85 | 27, 84 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun 𝐻 |
86 | | vex 3412 |
. . . . . . . . . . 11
⊢ 𝑐 ∈ V |
87 | | resfunexg 7031 |
. . . . . . . . . . 11
⊢ ((Fun
𝐻 ∧ 𝑐 ∈ V) → (𝐻 ↾ 𝑐) ∈ V) |
88 | 85, 86, 87 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐻 ↾ 𝑐) ∈ V |
89 | | sbceq1a 3705 |
. . . . . . . . . 10
⊢ (𝑑 = (𝐻 ↾ 𝑐) → ([𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐))) |
90 | 83, 88, 89 | ceqsal 3442 |
. . . . . . . . 9
⊢
(∀𝑑(𝑑 = (𝐻 ↾ 𝑐) → [𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) ↔ [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) |
91 | 82, 90 | sylib 221 |
. . . . . . . 8
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐)) |
92 | | sbccow 3717 |
. . . . . . . 8
⊢
([(𝐻 ↾
𝑐) / 𝑑][𝑑 / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐)) |
93 | 91, 92 | sylib 221 |
. . . . . . 7
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → [(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐)) |
94 | | nfcsb1v 3836 |
. . . . . . . . . 10
⊢
Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 |
95 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑅1‘𝑐) |
96 | 94, 95 | nfwe 5527 |
. . . . . . . . 9
⊢
Ⅎ𝑧⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐) |
97 | | csbeq1a 3825 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐻 ↾ 𝑐) → 𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺) |
98 | | weeq1 5539 |
. . . . . . . . . 10
⊢ (𝐺 = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
99 | 97, 98 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 = (𝐻 ↾ 𝑐) → (𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
100 | 96, 99 | sbciegf 3733 |
. . . . . . . 8
⊢ ((𝐻 ↾ 𝑐) ∈ V → ([(𝐻 ↾ 𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
101 | 88, 100 | ax-mp 5 |
. . . . . . 7
⊢
([(𝐻 ↾
𝑐) / 𝑧]𝐺 We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)) |
102 | 93, 101 | sylib 221 |
. . . . . 6
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐)) |
103 | | recsval 8140 |
. . . . . . . . 9
⊢ (𝑐 ∈ On → (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐))) |
104 | 26 | fveq1i 6718 |
. . . . . . . . 9
⊢ (𝐻‘𝑐) = (recs((𝑧 ∈ V ↦ 𝐺))‘𝑐) |
105 | | fvex 6730 |
. . . . . . . . . . . . . . 15
⊢
(𝑅1‘dom 𝑧) ∈ V |
106 | 105, 105 | xpex 7538 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘dom 𝑧) × (𝑅1‘dom
𝑧)) ∈
V |
107 | 106 | inex2 5211 |
. . . . . . . . . . . . 13
⊢ (if(dom
𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) ∈ V |
108 | 21, 107 | eqeltri 2834 |
. . . . . . . . . . . 12
⊢ 𝐺 ∈ V |
109 | 108 | csbex 5204 |
. . . . . . . . . . 11
⊢
⦋(𝐻
↾ 𝑐) / 𝑧⦌𝐺 ∈ V |
110 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ V ↦ 𝐺) = (𝑧 ∈ V ↦ 𝐺) |
111 | 110 | fvmpts 6821 |
. . . . . . . . . . 11
⊢ (((𝐻 ↾ 𝑐) ∈ V ∧ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 ∈ V) → ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺) |
112 | 88, 109, 111 | mp2an 692 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 |
113 | 26 | reseq1i 5847 |
. . . . . . . . . . 11
⊢ (𝐻 ↾ 𝑐) = (recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐) |
114 | 113 | fveq2i 6720 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ V ↦ 𝐺)‘(𝐻 ↾ 𝑐)) = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)) |
115 | 112, 114 | eqtr3i 2767 |
. . . . . . . . 9
⊢
⦋(𝐻
↾ 𝑐) / 𝑧⦌𝐺 = ((𝑧 ∈ V ↦ 𝐺)‘(recs((𝑧 ∈ V ↦ 𝐺)) ↾ 𝑐)) |
116 | 103, 104,
115 | 3eqtr4g 2803 |
. . . . . . . 8
⊢ (𝑐 ∈ On → (𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺) |
117 | | weeq1 5539 |
. . . . . . . 8
⊢ ((𝐻‘𝑐) = ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
118 | 116, 117 | syl 17 |
. . . . . . 7
⊢ (𝑐 ∈ On → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
119 | 118 | 3ad2ant1 1135 |
. . . . . 6
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → ((𝐻‘𝑐) We (𝑅1‘𝑐) ↔ ⦋(𝐻 ↾ 𝑐) / 𝑧⦌𝐺 We (𝑅1‘𝑐))) |
120 | 102, 119 | mpbird 260 |
. . . . 5
⊢ ((𝑐 ∈ On ∧ ∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) ∧ (𝜑 ∧ 𝑐 ⊆ 𝐴)) → (𝐻‘𝑐) We (𝑅1‘𝑐)) |
121 | 120 | 3exp 1121 |
. . . 4
⊢ (𝑐 ∈ On → (∀𝑑 ∈ 𝑐 ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (𝐻‘𝑑) We (𝑅1‘𝑑)) → ((𝜑 ∧ 𝑐 ⊆ 𝐴) → (𝐻‘𝑐) We (𝑅1‘𝑐)))) |
122 | 9, 15, 121 | tfis3 7636 |
. . 3
⊢ (𝐴 ∈ On → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴))) |
123 | 3, 122 | mpcom 38 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝐻‘𝐴) We (𝑅1‘𝐴)) |
124 | 1, 123 | mpan2 691 |
1
⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴)) |