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 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ { 𝑥 ∈ 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 ∣ 𝑥 ≼ 𝐴 } ) )