Metamath Proof Explorer


Theorem hartogslem1

Description: Lemma for hartogs . (Contributed by Mario Carneiro, 14-Jan-2013) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses hartogslem.2 𝐹 = { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
hartogslem.3 𝑅 = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤𝑦𝑧𝑦 ( ( 𝑠 = ( 𝑓𝑤 ) ∧ 𝑡 = ( 𝑓𝑧 ) ) ∧ 𝑤 E 𝑧 ) }
Assertion hartogslem1 ( dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) ∧ Fun 𝐹 ∧ ( 𝐴𝑉 → ran 𝐹 = { 𝑥 ∈ On ∣ 𝑥𝐴 } ) )

Proof

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 ∣ 𝑥𝐴 } ) )