Step |
Hyp |
Ref |
Expression |
1 |
|
hartogslem.2 |
⊢ 𝐹 = { 〈 𝑟 , 𝑦 〉 ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } |
2 |
|
hartogslem.3 |
⊢ 𝑅 = { 〈 𝑠 , 𝑡 〉 ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑓 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑓 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) } |
3 |
1
|
dmeqi |
⊢ dom 𝐹 = dom { 〈 𝑟 , 𝑦 〉 ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } |
4 |
|
dmopab |
⊢ 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 𝑟 ) ) } |
5 |
3 4
|
eqtri |
⊢ dom 𝐹 = { 𝑟 ∣ ∃ 𝑦 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } |
6 |
|
simp3 |
⊢ ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) → 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) |
7 |
|
simp1 |
⊢ ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) → dom 𝑟 ⊆ 𝐴 ) |
8 |
|
xpss12 |
⊢ ( ( dom 𝑟 ⊆ 𝐴 ∧ dom 𝑟 ⊆ 𝐴 ) → ( dom 𝑟 × dom 𝑟 ) ⊆ ( 𝐴 × 𝐴 ) ) |
9 |
7 7 8
|
syl2anc |
⊢ ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) → ( dom 𝑟 × dom 𝑟 ) ⊆ ( 𝐴 × 𝐴 ) ) |
10 |
6 9
|
sstrd |
⊢ ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) → 𝑟 ⊆ ( 𝐴 × 𝐴 ) ) |
11 |
|
velpw |
⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ↔ 𝑟 ⊆ ( 𝐴 × 𝐴 ) ) |
12 |
10 11
|
sylibr |
⊢ ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) |
13 |
12
|
ad2antrr |
⊢ ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) |
14 |
13
|
exlimiv |
⊢ ( ∃ 𝑦 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) |
15 |
14
|
abssi |
⊢ { 𝑟 ∣ ∃ 𝑦 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ⊆ 𝒫 ( 𝐴 × 𝐴 ) |
16 |
5 15
|
eqsstri |
⊢ dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) |
17 |
|
funopab4 |
⊢ Fun { 〈 𝑟 , 𝑦 〉 ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } |
18 |
1
|
funeqi |
⊢ ( Fun 𝐹 ↔ Fun { 〈 𝑟 , 𝑦 〉 ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ) |
19 |
17 18
|
mpbir |
⊢ Fun 𝐹 |
20 |
1
|
rneqi |
⊢ ran 𝐹 = ran { 〈 𝑟 , 𝑦 〉 ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } |
21 |
|
rnopab |
⊢ 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 𝑟 ) ) } |
22 |
20 21
|
eqtri |
⊢ ran 𝐹 = { 𝑦 ∣ ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } |
23 |
|
breq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≼ 𝐴 ↔ 𝑦 ≼ 𝐴 ) ) |
24 |
23
|
elrab |
⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ↔ ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) |
25 |
|
f1f |
⊢ ( 𝑓 : 𝑦 –1-1→ 𝐴 → 𝑓 : 𝑦 ⟶ 𝐴 ) |
26 |
25
|
adantl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → 𝑓 : 𝑦 ⟶ 𝐴 ) |
27 |
26
|
frnd |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ran 𝑓 ⊆ 𝐴 ) |
28 |
|
resss |
⊢ ( I ↾ ran 𝑓 ) ⊆ I |
29 |
|
ssun2 |
⊢ I ⊆ ( 𝑅 ∪ I ) |
30 |
28 29
|
sstri |
⊢ ( I ↾ ran 𝑓 ) ⊆ ( 𝑅 ∪ I ) |
31 |
|
idssxp |
⊢ ( I ↾ ran 𝑓 ) ⊆ ( ran 𝑓 × ran 𝑓 ) |
32 |
30 31
|
ssini |
⊢ ( I ↾ ran 𝑓 ) ⊆ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) |
33 |
32
|
a1i |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( I ↾ ran 𝑓 ) ⊆ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ) |
34 |
|
inss2 |
⊢ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ⊆ ( ran 𝑓 × ran 𝑓 ) |
35 |
34
|
a1i |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ⊆ ( ran 𝑓 × ran 𝑓 ) ) |
36 |
27 33 35
|
3jca |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( ran 𝑓 ⊆ 𝐴 ∧ ( I ↾ ran 𝑓 ) ⊆ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ∧ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ⊆ ( ran 𝑓 × ran 𝑓 ) ) ) |
37 |
|
eloni |
⊢ ( 𝑦 ∈ On → Ord 𝑦 ) |
38 |
|
ordwe |
⊢ ( Ord 𝑦 → E We 𝑦 ) |
39 |
37 38
|
syl |
⊢ ( 𝑦 ∈ On → E We 𝑦 ) |
40 |
39
|
adantr |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → E We 𝑦 ) |
41 |
|
f1f1orn |
⊢ ( 𝑓 : 𝑦 –1-1→ 𝐴 → 𝑓 : 𝑦 –1-1-onto→ ran 𝑓 ) |
42 |
41
|
adantl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → 𝑓 : 𝑦 –1-1-onto→ ran 𝑓 ) |
43 |
|
f1oiso |
⊢ ( ( 𝑓 : 𝑦 –1-1-onto→ ran 𝑓 ∧ 𝑅 = { 〈 𝑠 , 𝑡 〉 ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑓 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑓 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) } ) → 𝑓 Isom E , 𝑅 ( 𝑦 , ran 𝑓 ) ) |
44 |
42 2 43
|
sylancl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → 𝑓 Isom E , 𝑅 ( 𝑦 , ran 𝑓 ) ) |
45 |
|
isores2 |
⊢ ( 𝑓 Isom E , 𝑅 ( 𝑦 , ran 𝑓 ) ↔ 𝑓 Isom E , ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ( 𝑦 , ran 𝑓 ) ) |
46 |
44 45
|
sylib |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → 𝑓 Isom E , ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ( 𝑦 , ran 𝑓 ) ) |
47 |
|
isowe |
⊢ ( 𝑓 Isom E , ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ( 𝑦 , ran 𝑓 ) → ( E We 𝑦 ↔ ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) We ran 𝑓 ) ) |
48 |
46 47
|
syl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( E We 𝑦 ↔ ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) We ran 𝑓 ) ) |
49 |
40 48
|
mpbid |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) We ran 𝑓 ) |
50 |
|
weso |
⊢ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) We ran 𝑓 → ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) Or ran 𝑓 ) |
51 |
49 50
|
syl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) Or ran 𝑓 ) |
52 |
|
inss2 |
⊢ ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ⊆ ( ran 𝑓 × ran 𝑓 ) |
53 |
52
|
brel |
⊢ ( 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 → ( 𝑥 ∈ ran 𝑓 ∧ 𝑥 ∈ ran 𝑓 ) ) |
54 |
53
|
simpld |
⊢ ( 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 → 𝑥 ∈ ran 𝑓 ) |
55 |
|
sonr |
⊢ ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) Or ran 𝑓 ∧ 𝑥 ∈ ran 𝑓 ) → ¬ 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 ) |
56 |
51 54 55
|
syl2an |
⊢ ( ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) ∧ 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 ) → ¬ 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 ) |
57 |
56
|
pm2.01da |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ¬ 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 ) |
58 |
57
|
alrimiv |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ∀ 𝑥 ¬ 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 ) |
59 |
|
intirr |
⊢ ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∩ I ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) 𝑥 ) |
60 |
58 59
|
sylibr |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∩ I ) = ∅ ) |
61 |
|
disj3 |
⊢ ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∩ I ) = ∅ ↔ ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ) |
62 |
60 61
|
sylib |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ) |
63 |
|
weeq1 |
⊢ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) → ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) We ran 𝑓 ↔ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We ran 𝑓 ) ) |
64 |
62 63
|
syl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) We ran 𝑓 ↔ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We ran 𝑓 ) ) |
65 |
49 64
|
mpbid |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We ran 𝑓 ) |
66 |
37
|
adantr |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → Ord 𝑦 ) |
67 |
|
isoeq3 |
⊢ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) → ( 𝑓 Isom E , ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ( 𝑦 , ran 𝑓 ) ↔ 𝑓 Isom E , ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ( 𝑦 , ran 𝑓 ) ) ) |
68 |
62 67
|
syl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( 𝑓 Isom E , ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ( 𝑦 , ran 𝑓 ) ↔ 𝑓 Isom E , ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ( 𝑦 , ran 𝑓 ) ) ) |
69 |
46 68
|
mpbid |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → 𝑓 Isom E , ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ( 𝑦 , ran 𝑓 ) ) |
70 |
|
vex |
⊢ 𝑓 ∈ V |
71 |
70
|
rnex |
⊢ ran 𝑓 ∈ V |
72 |
|
exse |
⊢ ( ran 𝑓 ∈ V → ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) Se ran 𝑓 ) |
73 |
71 72
|
ax-mp |
⊢ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) Se ran 𝑓 |
74 |
|
eqid |
⊢ OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) |
75 |
74
|
oieu |
⊢ ( ( ( ( 𝑅 ∩ ( 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 𝑓 ) ) ) ) |
76 |
65 73 75
|
sylancl |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( ( Ord 𝑦 ∧ 𝑓 Isom E , ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ( 𝑦 , ran 𝑓 ) ) ↔ ( 𝑦 = dom OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ∧ 𝑓 = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) ) ) |
77 |
66 69 76
|
mpbi2and |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ( 𝑦 = dom OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ∧ 𝑓 = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) ) |
78 |
77
|
simpld |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → 𝑦 = dom OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) |
79 |
71 71
|
xpex |
⊢ ( ran 𝑓 × ran 𝑓 ) ∈ V |
80 |
79
|
inex2 |
⊢ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ∈ V |
81 |
|
sseq1 |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( 𝑟 ⊆ ( ran 𝑓 × ran 𝑓 ) ↔ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ⊆ ( ran 𝑓 × ran 𝑓 ) ) ) |
82 |
34 81
|
mpbiri |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → 𝑟 ⊆ ( ran 𝑓 × ran 𝑓 ) ) |
83 |
|
dmss |
⊢ ( 𝑟 ⊆ ( ran 𝑓 × ran 𝑓 ) → dom 𝑟 ⊆ dom ( ran 𝑓 × ran 𝑓 ) ) |
84 |
82 83
|
syl |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → dom 𝑟 ⊆ dom ( ran 𝑓 × ran 𝑓 ) ) |
85 |
|
dmxpid |
⊢ dom ( ran 𝑓 × ran 𝑓 ) = ran 𝑓 |
86 |
84 85
|
sseqtrdi |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → dom 𝑟 ⊆ ran 𝑓 ) |
87 |
|
dmresi |
⊢ dom ( I ↾ ran 𝑓 ) = ran 𝑓 |
88 |
|
sseq2 |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( ( I ↾ ran 𝑓 ) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓 ) ⊆ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ) ) |
89 |
32 88
|
mpbiri |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( I ↾ ran 𝑓 ) ⊆ 𝑟 ) |
90 |
|
dmss |
⊢ ( ( I ↾ ran 𝑓 ) ⊆ 𝑟 → dom ( I ↾ ran 𝑓 ) ⊆ dom 𝑟 ) |
91 |
89 90
|
syl |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → dom ( I ↾ ran 𝑓 ) ⊆ dom 𝑟 ) |
92 |
87 91
|
eqsstrrid |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ran 𝑓 ⊆ dom 𝑟 ) |
93 |
86 92
|
eqssd |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → dom 𝑟 = ran 𝑓 ) |
94 |
93
|
sseq1d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( dom 𝑟 ⊆ 𝐴 ↔ ran 𝑓 ⊆ 𝐴 ) ) |
95 |
93
|
reseq2d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( I ↾ dom 𝑟 ) = ( I ↾ ran 𝑓 ) ) |
96 |
|
id |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ) |
97 |
95 96
|
sseq12d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓 ) ⊆ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ) ) |
98 |
93
|
sqxpeqd |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( dom 𝑟 × dom 𝑟 ) = ( ran 𝑓 × ran 𝑓 ) ) |
99 |
96 98
|
sseq12d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ↔ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ⊆ ( ran 𝑓 × ran 𝑓 ) ) ) |
100 |
94 97 99
|
3anbi123d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ↔ ( ran 𝑓 ⊆ 𝐴 ∧ ( I ↾ ran 𝑓 ) ⊆ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ∧ ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ⊆ ( ran 𝑓 × ran 𝑓 ) ) ) ) |
101 |
|
difeq1 |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( 𝑟 ∖ I ) = ( ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ) |
102 |
|
difun2 |
⊢ ( ( 𝑅 ∪ I ) ∖ I ) = ( 𝑅 ∖ I ) |
103 |
102
|
ineq1i |
⊢ ( ( ( 𝑅 ∪ I ) ∖ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) = ( ( 𝑅 ∖ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) |
104 |
|
indif1 |
⊢ ( ( ( 𝑅 ∪ I ) ∖ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) = ( ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) |
105 |
|
indif1 |
⊢ ( ( 𝑅 ∖ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) |
106 |
103 104 105
|
3eqtr3i |
⊢ ( ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) |
107 |
101 106
|
eqtrdi |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( 𝑟 ∖ I ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) ) |
108 |
|
weeq1 |
⊢ ( ( 𝑟 ∖ I ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) → ( ( 𝑟 ∖ I ) We dom 𝑟 ↔ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We dom 𝑟 ) ) |
109 |
107 108
|
syl |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( ( 𝑟 ∖ I ) We dom 𝑟 ↔ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We dom 𝑟 ) ) |
110 |
|
weeq2 |
⊢ ( dom 𝑟 = ran 𝑓 → ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We dom 𝑟 ↔ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We ran 𝑓 ) ) |
111 |
93 110
|
syl |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We dom 𝑟 ↔ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We ran 𝑓 ) ) |
112 |
109 111
|
bitrd |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( ( 𝑟 ∖ I ) We dom 𝑟 ↔ ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) We ran 𝑓 ) ) |
113 |
100 112
|
anbi12d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ 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 𝑓 ) ) ) |
114 |
|
oieq1 |
⊢ ( ( 𝑟 ∖ I ) = ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) → OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , dom 𝑟 ) ) |
115 |
107 114
|
syl |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , dom 𝑟 ) ) |
116 |
|
oieq2 |
⊢ ( dom 𝑟 = ran 𝑓 → OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , dom 𝑟 ) = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) |
117 |
93 116
|
syl |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , dom 𝑟 ) = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) |
118 |
115 117
|
eqtrd |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) = OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) |
119 |
118
|
dmeqd |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) = dom OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) |
120 |
119
|
eqeq2d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ I ) ∩ ( ran 𝑓 × ran 𝑓 ) ) → ( 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ↔ 𝑦 = dom OrdIso ( ( ( 𝑅 ∩ ( ran 𝑓 × ran 𝑓 ) ) ∖ I ) , ran 𝑓 ) ) ) |
121 |
113 120
|
anbi12d |
⊢ ( 𝑟 = ( ( 𝑅 ∪ 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 𝑓 ) ) ) ) |
122 |
80 121
|
spcev |
⊢ ( ( ( ( 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 𝑟 ) ) ) |
123 |
36 65 78 122
|
syl21anc |
⊢ ( ( 𝑦 ∈ On ∧ 𝑓 : 𝑦 –1-1→ 𝐴 ) → ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) |
124 |
123
|
ex |
⊢ ( 𝑦 ∈ On → ( 𝑓 : 𝑦 –1-1→ 𝐴 → ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) ) |
125 |
124
|
exlimdv |
⊢ ( 𝑦 ∈ On → ( ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝐴 → ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) ) |
126 |
|
brdomi |
⊢ ( 𝑦 ≼ 𝐴 → ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝐴 ) |
127 |
125 126
|
impel |
⊢ ( ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) → ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) |
128 |
|
simpr |
⊢ ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) |
129 |
|
vex |
⊢ 𝑟 ∈ V |
130 |
129
|
dmex |
⊢ dom 𝑟 ∈ V |
131 |
|
eqid |
⊢ OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) = OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) |
132 |
131
|
oion |
⊢ ( dom 𝑟 ∈ V → dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ∈ On ) |
133 |
130 132
|
ax-mp |
⊢ dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ∈ On |
134 |
128 133
|
eqeltrdi |
⊢ ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → 𝑦 ∈ On ) |
135 |
134
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) → 𝑦 ∈ On ) |
136 |
|
simplr |
⊢ ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → ( 𝑟 ∖ I ) We dom 𝑟 ) |
137 |
131
|
oien |
⊢ ( ( dom 𝑟 ∈ V ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) → dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ≈ dom 𝑟 ) |
138 |
130 136 137
|
sylancr |
⊢ ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ≈ dom 𝑟 ) |
139 |
128 138
|
eqbrtrd |
⊢ ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → 𝑦 ≈ dom 𝑟 ) |
140 |
|
ssdomg |
⊢ ( 𝐴 ∈ 𝑉 → ( dom 𝑟 ⊆ 𝐴 → dom 𝑟 ≼ 𝐴 ) ) |
141 |
|
simpll1 |
⊢ ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → dom 𝑟 ⊆ 𝐴 ) |
142 |
140 141
|
impel |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) → dom 𝑟 ≼ 𝐴 ) |
143 |
|
endomtr |
⊢ ( ( 𝑦 ≈ dom 𝑟 ∧ dom 𝑟 ≼ 𝐴 ) → 𝑦 ≼ 𝐴 ) |
144 |
139 142 143
|
syl2an2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) → 𝑦 ≼ 𝐴 ) |
145 |
135 144
|
jca |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) |
146 |
145
|
ex |
⊢ ( 𝐴 ∈ 𝑉 → ( ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) ) |
147 |
146
|
exlimdv |
⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) ) |
148 |
127 147
|
impbid2 |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ↔ ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) ) |
149 |
24 148
|
syl5bb |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ↔ ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) ) ) |
150 |
149
|
abbi2dv |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } = { 𝑦 ∣ ∃ 𝑟 ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ) |
151 |
22 150
|
eqtr4id |
⊢ ( 𝐴 ∈ 𝑉 → ran 𝐹 = { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) |
152 |
16 19 151
|
3pm3.2i |
⊢ ( dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) ∧ Fun 𝐹 ∧ ( 𝐴 ∈ 𝑉 → ran 𝐹 = { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) ) |