Proof of Theorem hartogslem1
Step | Hyp | Ref
| Expression |
1 | | hartogslem.2 |
. . . . 5
⊢ 𝐹 = {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
2 | 1 | dmeqi 5247 |
. . . 4
⊢ dom 𝐹 = dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
3 | | dmopab 5257 |
. . . 4
⊢ dom
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = {𝑟 ∣ ∃𝑦(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
4 | 2, 3 | eqtri 2632 |
. . 3
⊢ dom 𝐹 = {𝑟 ∣ ∃𝑦(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
5 | | simp3 1056 |
. . . . . . . 8
⊢ ((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) |
6 | | simp1 1054 |
. . . . . . . . 9
⊢ ((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → dom 𝑟 ⊆ 𝐴) |
7 | | xpss12 5148 |
. . . . . . . . 9
⊢ ((dom
𝑟 ⊆ 𝐴 ∧ dom 𝑟 ⊆ 𝐴) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴)) |
8 | 6, 6, 7 | syl2anc 691 |
. . . . . . . 8
⊢ ((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴)) |
9 | 5, 8 | sstrd 3578 |
. . . . . . 7
⊢ ((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (𝐴 × 𝐴)) |
10 | | selpw 4115 |
. . . . . . 7
⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴)) |
11 | 9, 10 | sylibr 223 |
. . . . . 6
⊢ ((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴)) |
12 | 11 | ad2antrr 758 |
. . . . 5
⊢ ((((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴)) |
13 | 12 | exlimiv 1845 |
. . . 4
⊢
(∃𝑦(((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴)) |
14 | 13 | abssi 3640 |
. . 3
⊢ {𝑟 ∣ ∃𝑦(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝐴 × 𝐴) |
15 | 4, 14 | eqsstri 3598 |
. 2
⊢ dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) |
16 | | funopab4 5839 |
. . 3
⊢ Fun
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
17 | 1 | funeqi 5824 |
. . 3
⊢ (Fun
𝐹 ↔ Fun {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}) |
18 | 16, 17 | mpbir 220 |
. 2
⊢ Fun 𝐹 |
19 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ≼ 𝐴 ↔ 𝑦 ≼ 𝐴)) |
20 | 19 | elrab 3331 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
21 | | brdomi 7852 |
. . . . . . 7
⊢ (𝑦 ≼ 𝐴 → ∃𝑓 𝑓:𝑦–1-1→𝐴) |
22 | | f1f 6014 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝑦–1-1→𝐴 → 𝑓:𝑦⟶𝐴) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → 𝑓:𝑦⟶𝐴) |
24 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝑦⟶𝐴 → ran 𝑓 ⊆ 𝐴) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ran 𝑓 ⊆ 𝐴) |
26 | | resss 5342 |
. . . . . . . . . . . . . . 15
⊢ ( I
↾ ran 𝑓) ⊆
I |
27 | | ssun2 3739 |
. . . . . . . . . . . . . . 15
⊢ I
⊆ (𝑅 ∪ I
) |
28 | 26, 27 | sstri 3577 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ ran 𝑓) ⊆
(𝑅 ∪ I
) |
29 | | f1oi 6086 |
. . . . . . . . . . . . . . 15
⊢ ( I
↾ ran 𝑓):ran 𝑓–1-1-onto→ran
𝑓 |
30 | | f1of 6050 |
. . . . . . . . . . . . . . 15
⊢ (( I
↾ ran 𝑓):ran 𝑓–1-1-onto→ran
𝑓 → ( I ↾ ran
𝑓):ran 𝑓⟶ran 𝑓) |
31 | | fssxp 5973 |
. . . . . . . . . . . . . . 15
⊢ (( I
↾ ran 𝑓):ran 𝑓⟶ran 𝑓 → ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓)) |
32 | 29, 30, 31 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ ran 𝑓) ⊆ (ran
𝑓 × ran 𝑓) |
33 | 28, 32 | ssini 3798 |
. . . . . . . . . . . . 13
⊢ ( I
↾ ran 𝑓) ⊆
((𝑅 ∪ I ) ∩ (ran
𝑓 × ran 𝑓)) |
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))) |
35 | | inss2 3796 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓) |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)) |
37 | 25, 34, 36 | 3jca 1235 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → (ran 𝑓 ⊆ 𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))) |
38 | | eloni 5650 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ On → Ord 𝑦) |
39 | | ordwe 5653 |
. . . . . . . . . . . . . . 15
⊢ (Ord
𝑦 → E We 𝑦) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ On → E We 𝑦) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → E We 𝑦) |
42 | | f1f1orn 6061 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝑦–1-1→𝐴 → 𝑓:𝑦–1-1-onto→ran
𝑓) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → 𝑓:𝑦–1-1-onto→ran
𝑓) |
44 | | hartogslem.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝑅 = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} |
45 | | f1oiso 6501 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝑦–1-1-onto→ran
𝑓 ∧ 𝑅 = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓)) |
46 | 43, 44, 45 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓)) |
47 | | isores2 6483 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Isom E , 𝑅 (𝑦, ran 𝑓) ↔ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓)) |
48 | 46, 47 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓)) |
49 | | isowe 6499 |
. . . . . . . . . . . . . 14
⊢ (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) → ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓)) |
51 | 41, 50 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓) |
52 | | weso 5029 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓) |
54 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓) |
55 | 54 | brel 5090 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥 → (𝑥 ∈ ran 𝑓 ∧ 𝑥 ∈ ran 𝑓)) |
56 | 55 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥 → 𝑥 ∈ ran 𝑓) |
57 | | sonr 4980 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓 ∧ 𝑥 ∈ ran 𝑓) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) |
58 | 53, 56, 57 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) ∧ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) |
59 | 58 | pm2.01da 457 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) |
60 | 59 | alrimiv 1842 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) |
61 | | intirr 5433 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) |
62 | 60, 61 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅) |
63 | | disj3 3973 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )) |
64 | 62, 63 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )) |
65 | | weeq1 5026 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)) |
67 | 51, 66 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓) |
68 | 38 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → Ord 𝑦) |
69 | | isoeq3 6469 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓))) |
70 | 64, 69 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓))) |
71 | 48, 70 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)) |
72 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑓 ∈ V |
73 | 72 | rnex 6992 |
. . . . . . . . . . . . . . 15
⊢ ran 𝑓 ∈ V |
74 | | exse 5002 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑓 ∈ V → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓) |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓 |
76 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
OrdIso(((𝑅 ∩
(ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) |
77 | 76 | oieu 8327 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓 ∧ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓) → ((Ord 𝑦 ∧ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)) ↔ (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))) |
78 | 67, 75, 77 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ((Ord 𝑦 ∧ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)) ↔ (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))) |
79 | 68, 71, 78 | mpbi2and 958 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))) |
80 | 79 | simpld 474 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)) |
81 | 73, 73 | xpex 6860 |
. . . . . . . . . . . . 13
⊢ (ran
𝑓 × ran 𝑓) ∈ V |
82 | 81 | inex2 4728 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∈ V |
83 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (ran 𝑓 × ran 𝑓) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))) |
84 | 35, 83 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 ⊆ (ran 𝑓 × ran 𝑓)) |
85 | | dmss 5245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ⊆ (ran 𝑓 × ran 𝑓) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓)) |
87 | | dmxpid 5266 |
. . . . . . . . . . . . . . . . . 18
⊢ dom (ran
𝑓 × ran 𝑓) = ran 𝑓 |
88 | 86, 87 | syl6sseq 3614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ ran 𝑓) |
89 | | dmresi 5376 |
. . . . . . . . . . . . . . . . . 18
⊢ dom ( I
↾ ran 𝑓) = ran 𝑓 |
90 | | sseq2 3590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ ran 𝑓) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))) |
91 | 33, 90 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ ran 𝑓) ⊆ 𝑟) |
92 | | dmss 5245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (( I
↾ ran 𝑓) ⊆
𝑟 → dom ( I ↾
ran 𝑓) ⊆ dom 𝑟) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟) |
94 | 89, 93 | syl5eqssr 3613 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ran 𝑓 ⊆ dom 𝑟) |
95 | 88, 94 | eqssd 3585 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 = ran 𝑓) |
96 | 95 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟 ⊆ 𝐴 ↔ ran 𝑓 ⊆ 𝐴)) |
97 | 95 | reseq2d 5317 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ dom 𝑟) = ( I ↾ ran 𝑓)) |
98 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))) |
99 | 97, 98 | sseq12d 3597 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ dom 𝑟) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))) |
100 | 95 | sqxpeqd 5065 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟 × dom 𝑟) = (ran 𝑓 × ran 𝑓)) |
101 | 98, 100 | sseq12d 3597 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (dom 𝑟 × dom 𝑟) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))) |
102 | 96, 99, 101 | 3anbi123d 1391 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ↔ (ran 𝑓 ⊆ 𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))) |
103 | | difeq1 3683 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I )) |
104 | | difun2 4000 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∪ I ) ∖ I ) = (𝑅 ∖ I ) |
105 | 104 | ineq1i 3772 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∪ I ) ∖ I ) ∩
(ran 𝑓 × ran 𝑓)) = ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) |
106 | | indif1 3830 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∪ I ) ∖ I ) ∩
(ran 𝑓 × ran 𝑓)) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) |
107 | | indif1 3830 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) |
108 | 105, 106,
107 | 3eqtr3i 2640 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) |
109 | 103, 108 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )) |
110 | | weeq1 5026 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟)) |
112 | | weeq2 5027 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝑟 = ran 𝑓 → (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)) |
113 | 95, 112 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)) |
114 | 111, 113 | bitrd 267 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)) |
115 | 102, 114 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ↔ ((ran 𝑓 ⊆ 𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))) |
116 | | oieq1 8300 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟)) |
117 | 109, 116 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟)) |
118 | | oieq2 8301 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝑟 = ran 𝑓 → OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)) |
119 | 95, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)) |
120 | 117, 119 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)) |
121 | 120 | dmeqd 5248 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)) |
122 | 121 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟) ↔ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))) |
123 | 115, 122 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) ↔ (((ran 𝑓 ⊆ 𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓) ∧ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))) |
124 | 82, 123 | spcev 3273 |
. . . . . . . . . . 11
⊢ ((((ran
𝑓 ⊆ 𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓) ∧ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)) → ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) |
125 | 37, 67, 80, 124 | syl21anc 1317 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) → ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) |
126 | 125 | ex 449 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (𝑓:𝑦–1-1→𝐴 → ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))) |
127 | 126 | exlimdv 1848 |
. . . . . . . 8
⊢ (𝑦 ∈ On → (∃𝑓 𝑓:𝑦–1-1→𝐴 → ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))) |
128 | 127 | imp 444 |
. . . . . . 7
⊢ ((𝑦 ∈ On ∧ ∃𝑓 𝑓:𝑦–1-1→𝐴) → ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) |
129 | 21, 128 | sylan2 490 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝑦 ≼ 𝐴) → ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) |
130 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) |
131 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑟 ∈ V |
132 | 131 | dmex 6991 |
. . . . . . . . . . . 12
⊢ dom 𝑟 ∈ V |
133 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
OrdIso((𝑟 ∖ I
), dom 𝑟) = OrdIso((𝑟 ∖ I ), dom 𝑟) |
134 | 133 | oion 8324 |
. . . . . . . . . . . 12
⊢ (dom
𝑟 ∈ V → dom
OrdIso((𝑟 ∖ I ), dom
𝑟) ∈
On) |
135 | 132, 134 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom
OrdIso((𝑟 ∖ I ), dom
𝑟) ∈
On |
136 | 130, 135 | syl6eqel 2696 |
. . . . . . . . . 10
⊢ ((((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ∈ On) |
137 | 136 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ∈ On) |
138 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑟 ∖ I ) We dom 𝑟) |
139 | 133 | oien 8326 |
. . . . . . . . . . . . 13
⊢ ((dom
𝑟 ∈ V ∧ (𝑟 ∖ I ) We dom 𝑟) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟) |
140 | 132, 138,
139 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟) |
141 | 130, 140 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ ((((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ≈ dom 𝑟) |
142 | 141 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ≈ dom 𝑟) |
143 | | simpll1 1093 |
. . . . . . . . . . 11
⊢ ((((dom
𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom 𝑟 ⊆ 𝐴) |
144 | | ssdomg 7887 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (dom 𝑟 ⊆ 𝐴 → dom 𝑟 ≼ 𝐴)) |
145 | 144 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ dom 𝑟 ⊆ 𝐴) → dom 𝑟 ≼ 𝐴) |
146 | 143, 145 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → dom 𝑟 ≼ 𝐴) |
147 | | endomtr 7900 |
. . . . . . . . . 10
⊢ ((𝑦 ≈ dom 𝑟 ∧ dom 𝑟 ≼ 𝐴) → 𝑦 ≼ 𝐴) |
148 | 142, 146,
147 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ≼ 𝐴) |
149 | 137, 148 | jca 553 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴)) |
150 | 149 | ex 449 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))) |
151 | 150 | exlimdv 1848 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝐴))) |
152 | 129, 151 | impbid2 215 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((𝑦 ∈ On ∧ 𝑦 ≼ 𝐴) ↔ ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))) |
153 | 20, 152 | syl5bb 271 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ↔ ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))) |
154 | 153 | abbi2dv 2729 |
. . 3
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} = {𝑦 ∣ ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}) |
155 | 1 | rneqi 5273 |
. . . 4
⊢ ran 𝐹 = ran {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
156 | | rnopab 5291 |
. . . 4
⊢ ran
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = {𝑦 ∣ ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
157 | 155, 156 | eqtri 2632 |
. . 3
⊢ ran 𝐹 = {𝑦 ∣ ∃𝑟(((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
158 | 154, 157 | syl6reqr 2663 |
. 2
⊢ (𝐴 ∈ 𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}) |
159 | 15, 18, 158 | 3pm3.2i 1232 |
1
⊢ (dom
𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴 ∈ 𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) |