Proof of Theorem dfac12lem2
Step | Hyp | Ref
| Expression |
1 | | dfac12.4 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom
𝑥) ↦ if(dom 𝑥 = ∪
dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·𝑜
(rank‘𝑦))
+𝑜 ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) |
2 | 1 | tfr1 7380 |
. . . . . . . . . . . . 13
⊢ 𝐺 Fn On |
3 | | fnfun 5902 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn On → Fun 𝐺) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun 𝐺 |
5 | | dfac12.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ On) |
6 | | funimaexg 5889 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V) |
7 | 4, 5, 6 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 “ 𝐶) ∈ V) |
8 | | uniexg 6853 |
. . . . . . . . . . 11
⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺
“ 𝐶) ∈
V) |
9 | | rnexg 6990 |
. . . . . . . . . . 11
⊢ (∪ (𝐺
“ 𝐶) ∈ V →
ran ∪ (𝐺 “ 𝐶) ∈ V) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ∈
V) |
11 | | dfac12.8 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
12 | | f1f 6014 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧):(𝑅1‘𝑧)⟶On) |
13 | | fssxp 5973 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)⟶On → (𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On)) |
14 | | ssv 3588 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(𝑅1‘𝑧) ⊆ V |
15 | | xpss1 5151 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((𝑅1‘𝑧) ⊆ V →
((𝑅1‘𝑧) × On) ⊆ (V ×
On)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
((𝑅1‘𝑧) × On) ⊆ (V ×
On) |
17 | | sstr 3576 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) ∧
((𝑅1‘𝑧) × On) ⊆ (V × On)) →
(𝐺‘𝑧) ⊆ (V × On)) |
18 | 16, 17 | mpan2 703 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ⊆ (V × On)) |
19 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺‘𝑧) ∈ V |
20 | 19 | elpw 4114 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑧) ∈ 𝒫 (V × On) ↔
(𝐺‘𝑧) ⊆ (V × On)) |
21 | 18, 20 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
22 | 12, 13, 21 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
23 | 22 | ralimi 2936 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
24 | 11, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
25 | | onss 6882 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ On → 𝐶 ⊆ On) |
26 | 5, 25 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ⊆ On) |
27 | | fndm 5904 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 Fn On → dom 𝐺 = On) |
28 | 2, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ dom 𝐺 = On |
29 | 26, 28 | syl6sseqr 3615 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ⊆ dom 𝐺) |
30 | | funimass4 6157 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐺 ∧ 𝐶 ⊆ dom 𝐺) → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔
∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On))) |
31 | 4, 29, 30 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔
∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On))) |
32 | 24, 31 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 “ 𝐶) ⊆ 𝒫 (V ×
On)) |
33 | | sspwuni 4547 |
. . . . . . . . . . . . 13
⊢ ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔
∪ (𝐺 “ 𝐶) ⊆ (V × On)) |
34 | 32, 33 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ (𝐺
“ 𝐶) ⊆ (V
× On)) |
35 | | rnss 5275 |
. . . . . . . . . . . 12
⊢ (∪ (𝐺
“ 𝐶) ⊆ (V
× On) → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V ×
On)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ⊆ ran (V
× On)) |
37 | | rnxpss 5485 |
. . . . . . . . . . 11
⊢ ran (V
× On) ⊆ On |
38 | 36, 37 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ⊆
On) |
39 | | ssonuni 6878 |
. . . . . . . . . 10
⊢ (ran
∪ (𝐺 “ 𝐶) ∈ V → (ran ∪ (𝐺
“ 𝐶) ⊆ On
→ ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)) |
40 | 10, 38, 39 | sylc 63 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
41 | | suceloni 6905 |
. . . . . . . . 9
⊢ (∪ ran ∪ (𝐺 “ 𝐶) ∈ On → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
43 | 42 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
44 | | rankon 8541 |
. . . . . . 7
⊢
(rank‘𝑦)
∈ On |
45 | | omcl 7503 |
. . . . . . 7
⊢ ((suc
∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦)) ∈
On) |
46 | 43, 44, 45 | sylancl 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦)) ∈
On) |
47 | | rankr1ai 8544 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(𝑅1‘𝐶) → (rank‘𝑦) ∈ 𝐶) |
48 | 47 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ 𝐶) |
49 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 = ∪ 𝐶) |
50 | 48, 49 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ ∪ 𝐶) |
51 | | eloni 5650 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ On → Ord 𝐶) |
52 | 5, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Ord 𝐶) |
53 | 52 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → Ord 𝐶) |
54 | | ordsucuniel 6916 |
. . . . . . . . . . 11
⊢ (Ord
𝐶 → ((rank‘𝑦) ∈ ∪ 𝐶
↔ suc (rank‘𝑦)
∈ 𝐶)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((rank‘𝑦) ∈ ∪ 𝐶
↔ suc (rank‘𝑦)
∈ 𝐶)) |
56 | 50, 55 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc (rank‘𝑦) ∈ 𝐶) |
57 | 11 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
58 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑧 = suc (rank‘𝑦) → (𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦))) |
59 | | f1eq1 6009 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On)) |
61 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑧 = suc (rank‘𝑦) →
(𝑅1‘𝑧) = (𝑅1‘suc
(rank‘𝑦))) |
62 | | f1eq2 6010 |
. . . . . . . . . . . 12
⊢
((𝑅1‘𝑧) = (𝑅1‘suc
(rank‘𝑦)) →
((𝐺‘suc
(rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On)) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On)) |
64 | 60, 63 | bitrd 267 |
. . . . . . . . . 10
⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On)) |
65 | 64 | rspcv 3278 |
. . . . . . . . 9
⊢ (suc
(rank‘𝑦) ∈ 𝐶 → (∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On)) |
66 | 56, 57, 65 | sylc 63 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On) |
67 | | f1f 6014 |
. . . . . . . 8
⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))⟶On) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))⟶On) |
69 | | r1elwf 8542 |
. . . . . . . . 9
⊢ (𝑦 ∈
(𝑅1‘𝐶) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
70 | 69 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
71 | | rankidb 8546 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈
(𝑅1‘suc (rank‘𝑦))) |
72 | 70, 71 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) |
73 | 68, 72 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) |
74 | | oacl 7502 |
. . . . . 6
⊢ (((suc
∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦)) ∈ On
∧ ((𝐺‘suc
(rank‘𝑦))‘𝑦) ∈ On) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On) |
75 | 46, 73, 74 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On) |
76 | | dfac12.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On) |
77 | | f1f 6014 |
. . . . . . . 8
⊢ (𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On → 𝐹:𝒫
(har‘(𝑅1‘𝐴))⟶On) |
78 | 76, 77 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝒫
(har‘(𝑅1‘𝐴))⟶On) |
79 | 78 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫
(har‘(𝑅1‘𝐴))⟶On) |
80 | | imassrn 5396 |
. . . . . . . 8
⊢ (𝐻 “ 𝑦) ⊆ ran 𝐻 |
81 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘∪ 𝐶)
∈ V |
82 | 81 | rnex 6992 |
. . . . . . . . . . . . . 14
⊢ ran
(𝐺‘∪ 𝐶)
∈ V |
83 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ∈ On) |
84 | | onuni 6885 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ On → ∪ 𝐶
∈ On) |
85 | | sucidg 5720 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝐶
∈ On → ∪ 𝐶 ∈ suc ∪
𝐶) |
86 | 83, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ suc ∪ 𝐶) |
87 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → Ord 𝐶) |
88 | | orduniorsuc 6922 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Ord
𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
90 | 89 | orcanai 950 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶) |
91 | 86, 90 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ 𝐶) |
92 | 11 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
93 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ∪
𝐶 → (𝐺‘𝑧) = (𝐺‘∪ 𝐶)) |
94 | | f1eq1 6009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺‘𝑧) = (𝐺‘∪ 𝐶) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ∪
𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On)) |
96 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ∪
𝐶 →
(𝑅1‘𝑧) = (𝑅1‘∪ 𝐶)) |
97 | | f1eq2 6010 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((𝑅1‘𝑧) = (𝑅1‘∪ 𝐶)
→ ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ∪
𝐶 → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)) |
99 | 95, 98 | bitrd 267 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ∪
𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)) |
100 | 99 | rspcv 3278 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝐶
∈ 𝐶 →
(∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)) |
101 | 91, 92, 100 | sylc 63 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On) |
102 | | f1f 6014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On) |
103 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On → ran (𝐺‘∪ 𝐶) ⊆ On) |
104 | 101, 102,
103 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ⊆ On) |
105 | | epweon 6875 |
. . . . . . . . . . . . . . 15
⊢ E We
On |
106 | | wess 5025 |
. . . . . . . . . . . . . . 15
⊢ (ran
(𝐺‘∪ 𝐶)
⊆ On → ( E We On → E We ran (𝐺‘∪ 𝐶))) |
107 | 104, 105,
106 | mpisyl 21 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → E We ran (𝐺‘∪ 𝐶)) |
108 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ OrdIso( E
, ran (𝐺‘∪ 𝐶))
= OrdIso( E , ran (𝐺‘∪ 𝐶)) |
109 | 108 | oiiso 8325 |
. . . . . . . . . . . . . 14
⊢ ((ran
(𝐺‘∪ 𝐶)
∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶))
Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶))) |
110 | 82, 107, 109 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → OrdIso( E , ran (𝐺‘∪ 𝐶))
Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶))) |
111 | | isof1o 6473 |
. . . . . . . . . . . . 13
⊢ (OrdIso(
E , ran (𝐺‘∪ 𝐶))
Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran
(𝐺‘∪ 𝐶)) |
112 | | f1ocnv 6062 |
. . . . . . . . . . . . 13
⊢ (OrdIso(
E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran
(𝐺‘∪ 𝐶)
→ ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom
OrdIso( E , ran (𝐺‘∪ 𝐶))) |
113 | | f1of1 6049 |
. . . . . . . . . . . . 13
⊢ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom
OrdIso( E , ran (𝐺‘∪ 𝐶)) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
114 | 110, 111,
112, 113 | 4syl 19 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
115 | | f1f1orn 6061 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran
(𝐺‘∪ 𝐶)) |
116 | | f1of1 6049 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran
(𝐺‘∪ 𝐶)
→ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶)) |
117 | 101, 115,
116 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶)) |
118 | | f1co 6023 |
. . . . . . . . . . . 12
⊢ ((◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶)) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
119 | 114, 117,
118 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
120 | | dfac12.h |
. . . . . . . . . . . 12
⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) |
121 | | f1eq1 6009 |
. . . . . . . . . . . 12
⊢ (𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) → (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))) |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
123 | 119, 122 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
124 | | f1f 6014 |
. . . . . . . . . 10
⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → 𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
125 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶))
→ ran 𝐻 ⊆ dom
OrdIso( E , ran (𝐺‘∪ 𝐶))) |
126 | 123, 124,
125 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
127 | | harcl 8349 |
. . . . . . . . . . 11
⊢
(har‘(𝑅1‘𝐴)) ∈ On |
128 | 127 | onordi 5749 |
. . . . . . . . . 10
⊢ Ord
(har‘(𝑅1‘𝐴)) |
129 | 108 | oion 8324 |
. . . . . . . . . . . 12
⊢ (ran
(𝐺‘∪ 𝐶)
∈ V → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On) |
130 | 82, 129 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
∈ On) |
131 | 108 | oien 8326 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝐺‘∪ 𝐶)
∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
≈ ran (𝐺‘∪ 𝐶)) |
132 | 82, 107, 131 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
≈ ran (𝐺‘∪ 𝐶)) |
133 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(𝑅1‘∪ 𝐶) ∈ V |
134 | 133 | f1oen 7862 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran
(𝐺‘∪ 𝐶)
→ (𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶)) |
135 | | ensym 7891 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈
(𝑅1‘∪ 𝐶)) |
136 | 101, 115,
134, 135 | 4syl 19 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈
(𝑅1‘∪ 𝐶)) |
137 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(𝑅1‘𝐴) ∈ V |
138 | | dfac12.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ On) |
139 | 138 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐴 ∈ On) |
140 | | dfac12.6 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
141 | 140 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ 𝐴) |
142 | 141, 91 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ 𝐴) |
143 | | r1ord2 8527 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → (∪ 𝐶
∈ 𝐴 →
(𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴))) |
144 | 139, 142,
143 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴)) |
145 | | ssdomg 7887 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘𝐴) ∈ V →
((𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴) →
(𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴))) |
146 | 137, 144,
145 | mpsyl 66 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) |
147 | | endomtr 7900 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝐺‘∪ 𝐶)
≈ (𝑅1‘∪ 𝐶) ∧
(𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → ran (𝐺‘∪ 𝐶) ≼
(𝑅1‘𝐴)) |
148 | 136, 146,
147 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≼
(𝑅1‘𝐴)) |
149 | | endomtr 7900 |
. . . . . . . . . . . 12
⊢ ((dom
OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶)
∧ ran (𝐺‘∪ 𝐶)
≼ (𝑅1‘𝐴)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶))
≼ (𝑅1‘𝐴)) |
150 | 132, 148,
149 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
≼ (𝑅1‘𝐴)) |
151 | | elharval 8351 |
. . . . . . . . . . 11
⊢ (dom
OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈
(har‘(𝑅1‘𝐴)) ↔ (dom OrdIso( E , ran (𝐺‘∪ 𝐶))
∈ On ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼
(𝑅1‘𝐴))) |
152 | 130, 150,
151 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
∈ (har‘(𝑅1‘𝐴))) |
153 | | ordelss 5656 |
. . . . . . . . . 10
⊢ ((Ord
(har‘(𝑅1‘𝐴)) ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶))
∈ (har‘(𝑅1‘𝐴))) → dom OrdIso( E , ran (𝐺‘∪ 𝐶))
⊆ (har‘(𝑅1‘𝐴))) |
154 | 128, 152,
153 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
⊆ (har‘(𝑅1‘𝐴))) |
155 | 126, 154 | sstrd 3578 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆
(har‘(𝑅1‘𝐴))) |
156 | 80, 155 | syl5ss 3579 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ⊆
(har‘(𝑅1‘𝐴))) |
157 | | fvex 6113 |
. . . . . . . 8
⊢
(har‘(𝑅1‘𝐴)) ∈ V |
158 | 157 | elpw2 4755 |
. . . . . . 7
⊢ ((𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑦) ⊆
(har‘(𝑅1‘𝐴))) |
159 | 156, 158 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
160 | 79, 159 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐹‘(𝐻 “ 𝑦)) ∈ On) |
161 | 75, 160 | ifclda 4070 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On) |
162 | 161 | ex 449 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On)) |
163 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝐶 = ∪
𝐶 → if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦))) |
164 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝐶 = ∪
𝐶 → if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧))) |
165 | 163, 164 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝐶 = ∪
𝐶 → (if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ ((suc ∪
ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
166 | 165 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ ((suc ∪
ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
167 | 42 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
168 | | nsuceq0 5722 |
. . . . . . . 8
⊢ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅ |
169 | 168 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅) |
170 | 44 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ On) |
171 | | onsucuni 6920 |
. . . . . . . . . . 11
⊢ (ran
∪ (𝐺 “ 𝐶) ⊆ On → ran ∪ (𝐺
“ 𝐶) ⊆ suc
∪ ran ∪ (𝐺 “ 𝐶)) |
172 | 38, 171 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ⊆ suc
∪ ran ∪ (𝐺 “ 𝐶)) |
173 | 172 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran ∪ (𝐺
“ 𝐶) ⊆ suc
∪ ran ∪ (𝐺 “ 𝐶)) |
174 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐺 Fn On) |
175 | 26 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ On) |
176 | | fnfvima 6400 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶)) |
177 | 174, 175,
56, 176 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶)) |
178 | | elssuni 4403 |
. . . . . . . . . . 11
⊢ ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ ∪
(𝐺 “ 𝐶)) |
179 | | rnss 5275 |
. . . . . . . . . . 11
⊢ ((𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺
“ 𝐶) → ran
(𝐺‘suc
(rank‘𝑦)) ⊆ ran
∪ (𝐺 “ 𝐶)) |
180 | 177, 178,
179 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪
(𝐺 “ 𝐶)) |
181 | | f1fn 6015 |
. . . . . . . . . . . 12
⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc
(rank‘𝑦))) |
182 | 66, 181 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc
(rank‘𝑦))) |
183 | | fnfvelrn 6264 |
. . . . . . . . . . 11
⊢ (((𝐺‘suc (rank‘𝑦)) Fn
(𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) →
((𝐺‘suc
(rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦))) |
184 | 182, 72, 183 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦))) |
185 | 180, 184 | sseldd 3569 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran ∪
(𝐺 “ 𝐶)) |
186 | 173, 185 | sseldd 3569 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
187 | 186 | adantlrr 753 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
188 | | rankon 8541 |
. . . . . . . 8
⊢
(rank‘𝑧)
∈ On |
189 | 188 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑧) ∈ On) |
190 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1‘𝐶) ↔ 𝑧 ∈ (𝑅1‘𝐶))) |
191 | 190 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ↔ (𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)))) |
192 | 191 | anbi1d 737 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶))) |
193 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧)) |
194 | | suceq 5707 |
. . . . . . . . . . . . . 14
⊢
((rank‘𝑦) =
(rank‘𝑧) → suc
(rank‘𝑦) = suc
(rank‘𝑧)) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧)) |
196 | 195 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧))) |
197 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
198 | 196, 197 | fveq12d 6109 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) |
199 | 198 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶))) |
200 | 192, 199 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)))) |
201 | 200, 186 | chvarv 2251 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
202 | 201 | adantlrl 752 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
203 | | omopth2 7551 |
. . . . . . 7
⊢ (((suc
∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅) ∧ ((rank‘𝑦) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) ∧ ((rank‘𝑧) ∈ On ∧ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶))) → (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
204 | 167, 169,
170, 187, 189, 202, 203 | syl222anc 1334 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
205 | 194 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧)) |
206 | 205 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧))) |
207 | 206 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) |
208 | 207 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))) |
209 | 66 | adantlrr 753 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On) |
210 | 209 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On) |
211 | 72 | adantlrr 753 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) |
212 | 211 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) |
213 | | r1elwf 8542 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈
(𝑅1‘𝐶) → 𝑧 ∈ ∪
(𝑅1 “ On)) |
214 | | rankidb 8546 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ∈
(𝑅1‘suc (rank‘𝑧))) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(𝑅1‘𝐶) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑧))) |
216 | 215 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑧))) |
217 | 216 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑧))) |
218 | 205 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) →
(𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc
(rank‘𝑧))) |
219 | 217, 218 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑦))) |
220 | | f1fveq 6420 |
. . . . . . . . . . 11
⊢ (((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On ∧ (𝑦 ∈ (𝑅1‘suc
(rank‘𝑦)) ∧ 𝑧 ∈
(𝑅1‘suc (rank‘𝑦)))) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧)) |
221 | 210, 212,
219, 220 | syl12anc 1316 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧)) |
222 | 208, 221 | bitr3d 269 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧)) |
223 | 222 | biimpd 218 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧)) |
224 | 223 | expimpd 627 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧)) |
225 | 193, 198 | jca 553 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))) |
226 | 224, 225 | impbid1 214 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧)) |
227 | 166, 204,
226 | 3bitrd 293 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)) |
228 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
𝐶 = ∪ 𝐶
→ if(𝐶 = ∪ 𝐶,
((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = (𝐹‘(𝐻 “ 𝑦))) |
229 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
𝐶 = ∪ 𝐶
→ if(𝐶 = ∪ 𝐶,
((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = (𝐹‘(𝐻 “ 𝑧))) |
230 | 228, 229 | eqeq12d 2625 |
. . . . . . 7
⊢ (¬
𝐶 = ∪ 𝐶
→ (if(𝐶 = ∪ 𝐶,
((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)))) |
231 | 230 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)))) |
232 | 76 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On) |
233 | 159 | adantlrr 753 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
234 | 191 | anbi1d 737 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶))) |
235 | | imaeq2 5381 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐻 “ 𝑦) = (𝐻 “ 𝑧)) |
236 | 235 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴)))) |
237 | 234, 236 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴))) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴))))) |
238 | 237, 159 | chvarv 2251 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
239 | 238 | adantlrl 752 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
240 | | f1fveq 6420 |
. . . . . . 7
⊢ ((𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On ∧ ((𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴)) ∧ (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴)))) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧))) |
241 | 232, 233,
239, 240 | syl12anc 1316 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧))) |
242 | 123 | adantlrr 753 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
243 | | simplrl 796 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑦 ∈
(𝑅1‘𝐶)) |
244 | 90 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘𝐶) = (𝑅1‘suc ∪ 𝐶)) |
245 | | r1suc 8516 |
. . . . . . . . . . . 12
⊢ (∪ 𝐶
∈ On → (𝑅1‘suc ∪
𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
246 | 83, 84, 245 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘suc ∪ 𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
247 | 244, 246 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
248 | 247 | adantlrr 753 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) →
(𝑅1‘𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
249 | 243, 248 | eleqtrd 2690 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑦 ∈ 𝒫
(𝑅1‘∪ 𝐶)) |
250 | 249 | elpwid 4118 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑦 ⊆
(𝑅1‘∪ 𝐶)) |
251 | | simplrr 797 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑧 ∈
(𝑅1‘𝐶)) |
252 | 251, 248 | eleqtrd 2690 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑧 ∈ 𝒫
(𝑅1‘∪ 𝐶)) |
253 | 252 | elpwid 4118 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑧 ⊆
(𝑅1‘∪ 𝐶)) |
254 | | f1imaeq 6423 |
. . . . . . 7
⊢ ((𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝑦 ⊆ (𝑅1‘∪ 𝐶)
∧ 𝑧 ⊆
(𝑅1‘∪ 𝐶))) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧)) |
255 | 242, 250,
253, 254 | syl12anc 1316 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧)) |
256 | 231, 241,
255 | 3bitrd 293 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)) |
257 | 227, 256 | pm2.61dan 828 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)) |
258 | 257 | ex 449 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶)) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑧))
+𝑜 ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))) |
259 | 162, 258 | dom2lem 7881 |
. 2
⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On) |
260 | 138, 76, 1, 5, 120 | dfac12lem1 8848 |
. . 3
⊢ (𝜑 → (𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))))) |
261 | | f1eq1 6009 |
. . 3
⊢ ((𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))) → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)) |
262 | 260, 261 | syl 17 |
. 2
⊢ (𝜑 → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·𝑜
(rank‘𝑦))
+𝑜 ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)) |
263 | 259, 262 | mpbird 246 |
1
⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On) |