MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hartogslem1 Structured version   Visualization version   GIF version

Theorem hartogslem1 8654
Description: Lemma for hartogs 8656. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
hartogslem.2 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
hartogslem.3 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}
Assertion
Ref Expression
hartogslem1 (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴}))
Distinct variable groups:   𝑓,𝑠,𝑡,𝑤,𝑦,𝑧   𝑓,𝑟,𝑥,𝐴,𝑦   𝑅,𝑟,𝑥   𝑉,𝑟,𝑦
Allowed substitution hints:   𝐴(𝑧,𝑤,𝑡,𝑠)   𝑅(𝑦,𝑧,𝑤,𝑡,𝑓,𝑠)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑡,𝑓,𝑠,𝑟)   𝑉(𝑥,𝑧,𝑤,𝑡,𝑓,𝑠)

Proof of Theorem hartogslem1
StepHypRef Expression
1 hartogslem.2 . . . . 5 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
21dmeqi 5493 . . . 4 dom 𝐹 = dom {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
3 dmopab 5503 . . . 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 𝑟))}
42, 3eqtri 2787 . . 3 dom 𝐹 = {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
5 simp3 1168 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (dom 𝑟 × dom 𝑟))
6 simp1 1166 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → dom 𝑟𝐴)
7 xpss12 5292 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ dom 𝑟𝐴) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
86, 6, 7syl2anc 579 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
95, 8sstrd 3771 . . . . . . 7 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (𝐴 × 𝐴))
10 selpw 4322 . . . . . . 7 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
119, 10sylibr 225 . . . . . 6 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1211ad2antrr 717 . . . . 5 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1312exlimiv 2025 . . . 4 (∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1413abssi 3837 . . 3 {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝐴 × 𝐴)
154, 14eqsstri 3795 . 2 dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴)
16 funopab4 6105 . . 3 Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
171funeqi 6089 . . 3 (Fun 𝐹 ↔ Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1816, 17mpbir 222 . 2 Fun 𝐹
19 breq1 4812 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2019elrab 3519 . . . . 5 (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ (𝑦 ∈ On ∧ 𝑦𝐴))
21 brdomi 8171 . . . . . . 7 (𝑦𝐴 → ∃𝑓 𝑓:𝑦1-1𝐴)
22 f1f 6283 . . . . . . . . . . . . . 14 (𝑓:𝑦1-1𝐴𝑓:𝑦𝐴)
2322adantl 473 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦𝐴)
2423frnd 6230 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ran 𝑓𝐴)
25 resss 5597 . . . . . . . . . . . . . . 15 ( I ↾ ran 𝑓) ⊆ I
26 ssun2 3939 . . . . . . . . . . . . . . 15 I ⊆ (𝑅 ∪ I )
2725, 26sstri 3770 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ (𝑅 ∪ I )
28 f1oi 6357 . . . . . . . . . . . . . . 15 ( I ↾ ran 𝑓):ran 𝑓1-1-onto→ran 𝑓
29 f1of 6320 . . . . . . . . . . . . . . 15 (( I ↾ ran 𝑓):ran 𝑓1-1-onto→ran 𝑓 → ( I ↾ ran 𝑓):ran 𝑓⟶ran 𝑓)
30 fssxp 6242 . . . . . . . . . . . . . . 15 (( I ↾ ran 𝑓):ran 𝑓⟶ran 𝑓 → ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓))
3128, 29, 30mp2b 10 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓)
3227, 31ssini 3995 . . . . . . . . . . . . 13 ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))
3332a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
34 inss2 3993 . . . . . . . . . . . . 13 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
3534a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))
3624, 33, 353jca 1158 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
37 eloni 5918 . . . . . . . . . . . . . . 15 (𝑦 ∈ On → Ord 𝑦)
38 ordwe 5921 . . . . . . . . . . . . . . 15 (Ord 𝑦 → E We 𝑦)
3937, 38syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ On → E We 𝑦)
4039adantr 472 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → E We 𝑦)
41 f1f1orn 6331 . . . . . . . . . . . . . . . . 17 (𝑓:𝑦1-1𝐴𝑓:𝑦1-1-onto→ran 𝑓)
4241adantl 473 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦1-1-onto→ran 𝑓)
43 hartogslem.3 . . . . . . . . . . . . . . . 16 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}
44 f1oiso 6793 . . . . . . . . . . . . . . . 16 ((𝑓:𝑦1-1-onto→ran 𝑓𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
4542, 43, 44sylancl 580 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
46 isores2 6775 . . . . . . . . . . . . . . 15 (𝑓 Isom E , 𝑅 (𝑦, ran 𝑓) ↔ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
4745, 46sylib 209 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
48 isowe 6791 . . . . . . . . . . . . . 14 (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) → ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓))
4947, 48syl 17 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓))
5040, 49mpbid 223 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓)
51 weso 5268 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
53 inss2 3993 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
5453brel 5336 . . . . . . . . . . . . . . . . . . 19 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥 → (𝑥 ∈ ran 𝑓𝑥 ∈ ran 𝑓))
5554simpld 488 . . . . . . . . . . . . . . . . . 18 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥𝑥 ∈ ran 𝑓)
56 sonr 5219 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓𝑥 ∈ ran 𝑓) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5752, 55, 56syl2an 589 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) ∧ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5857pm2.01da 833 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5958alrimiv 2022 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
60 intirr 5697 . . . . . . . . . . . . . . 15 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
6159, 60sylibr 225 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅)
62 disj3 4182 . . . . . . . . . . . . . 14 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
6361, 62sylib 209 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
64 weeq1 5265 . . . . . . . . . . . . 13 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
6563, 64syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
6650, 65mpbid 223 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)
6737adantr 472 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → Ord 𝑦)
68 isoeq3 6761 . . . . . . . . . . . . . . 15 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)))
6963, 68syl 17 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)))
7047, 69mpbid 223 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓))
71 vex 3353 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
7271rnex 7298 . . . . . . . . . . . . . . 15 ran 𝑓 ∈ V
73 exse 5241 . . . . . . . . . . . . . . 15 (ran 𝑓 ∈ V → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓)
7472, 73ax-mp 5 . . . . . . . . . . . . . 14 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓
75 eqid 2765 . . . . . . . . . . . . . . 15 OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)
7675oieu 8651 . . . . . . . . . . . . . 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 𝑓))))
7766, 74, 76sylancl 580 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((Ord 𝑦𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)) ↔ (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))))
7867, 70, 77mpbi2and 703 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
7978simpld 488 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
8072, 72xpex 7160 . . . . . . . . . . . . 13 (ran 𝑓 × ran 𝑓) ∈ V
8180inex2 4961 . . . . . . . . . . . 12 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∈ V
82 sseq1 3786 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (ran 𝑓 × ran 𝑓) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
8334, 82mpbiri 249 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 ⊆ (ran 𝑓 × ran 𝑓))
84 dmss 5491 . . . . . . . . . . . . . . . . . . 19 (𝑟 ⊆ (ran 𝑓 × ran 𝑓) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
8583, 84syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
86 dmxpid 5513 . . . . . . . . . . . . . . . . . 18 dom (ran 𝑓 × ran 𝑓) = ran 𝑓
8785, 86syl6sseq 3811 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ ran 𝑓)
88 dmresi 5641 . . . . . . . . . . . . . . . . . 18 dom ( I ↾ ran 𝑓) = ran 𝑓
89 sseq2 3787 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ ran 𝑓) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
9032, 89mpbiri 249 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ ran 𝑓) ⊆ 𝑟)
91 dmss 5491 . . . . . . . . . . . . . . . . . . 19 (( I ↾ ran 𝑓) ⊆ 𝑟 → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9290, 91syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9388, 92syl5eqssr 3810 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ran 𝑓 ⊆ dom 𝑟)
9487, 93eqssd 3778 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 = ran 𝑓)
9594sseq1d 3792 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟𝐴 ↔ ran 𝑓𝐴))
9694reseq2d 5565 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ dom 𝑟) = ( I ↾ ran 𝑓))
97 id 22 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
9896, 97sseq12d 3794 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ dom 𝑟) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
9994sqxpeqd 5309 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟 × dom 𝑟) = (ran 𝑓 × ran 𝑓))
10097, 99sseq12d 3794 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (dom 𝑟 × dom 𝑟) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
10195, 98, 1003anbi123d 1560 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ↔ (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))))
102 difeq1 3883 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
103 difun2 4208 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∪ I ) ∖ I ) = (𝑅 ∖ I )
104103ineq1i 3972 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓))
105 indif1 4036 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
106 indif1 4036 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
107104, 105, 1063eqtr3i 2795 . . . . . . . . . . . . . . . . 17 (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
108102, 107syl6eq 2815 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
109 weeq1 5265 . . . . . . . . . . . . . . . 16 ((𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟))
110108, 109syl 17 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟))
111 weeq2 5266 . . . . . . . . . . . . . . . 16 (dom 𝑟 = ran 𝑓 → (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
11294, 111syl 17 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
113110, 112bitrd 270 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
114101, 113anbi12d 624 . . . . . . . . . . . . 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 𝑓)))
115 oieq1 8624 . . . . . . . . . . . . . . . . 17 ((𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟))
116108, 115syl 17 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟))
117 oieq2 8625 . . . . . . . . . . . . . . . . 17 (dom 𝑟 = ran 𝑓 → OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
11894, 117syl 17 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
119116, 118eqtrd 2799 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
120119dmeqd 5494 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
121120eqeq2d 2775 . . . . . . . . . . . . 13 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟) ↔ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
122114, 121anbi12d 624 . . . . . . . . . . . 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 𝑓))))
12381, 122spcev 3452 . . . . . . . . . . 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 𝑟)))
12436, 66, 79, 123syl21anc 866 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
125124ex 401 . . . . . . . . 9 (𝑦 ∈ On → (𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
126125exlimdv 2028 . . . . . . . 8 (𝑦 ∈ On → (∃𝑓 𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
127126imp 395 . . . . . . 7 ((𝑦 ∈ On ∧ ∃𝑓 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
12821, 127sylan2 586 . . . . . 6 ((𝑦 ∈ On ∧ 𝑦𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
129 simpr 477 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))
130 vex 3353 . . . . . . . . . . . . 13 𝑟 ∈ V
131130dmex 7297 . . . . . . . . . . . 12 dom 𝑟 ∈ V
132 eqid 2765 . . . . . . . . . . . . 13 OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso((𝑟 ∖ I ), dom 𝑟)
133132oion 8648 . . . . . . . . . . . 12 (dom 𝑟 ∈ V → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On)
134131, 133ax-mp 5 . . . . . . . . . . 11 dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On
135129, 134syl6eqel 2852 . . . . . . . . . 10 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ∈ On)
136135adantl 473 . . . . . . . . 9 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ∈ On)
137 simplr 785 . . . . . . . . . . . . 13 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑟 ∖ I ) We dom 𝑟)
138132oien 8650 . . . . . . . . . . . . 13 ((dom 𝑟 ∈ V ∧ (𝑟 ∖ I ) We dom 𝑟) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟)
139131, 137, 138sylancr 581 . . . . . . . . . . . 12 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟)
140129, 139eqbrtrd 4831 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ≈ dom 𝑟)
141140adantl 473 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ≈ dom 𝑟)
142 simpll1 1269 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom 𝑟𝐴)
143 ssdomg 8206 . . . . . . . . . . . 12 (𝐴𝑉 → (dom 𝑟𝐴 → dom 𝑟𝐴))
144143imp 395 . . . . . . . . . . 11 ((𝐴𝑉 ∧ dom 𝑟𝐴) → dom 𝑟𝐴)
145142, 144sylan2 586 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → dom 𝑟𝐴)
146 endomtr 8218 . . . . . . . . . 10 ((𝑦 ≈ dom 𝑟 ∧ dom 𝑟𝐴) → 𝑦𝐴)
147141, 145, 146syl2anc 579 . . . . . . . . 9 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦𝐴)
148136, 147jca 507 . . . . . . . 8 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → (𝑦 ∈ On ∧ 𝑦𝐴))
149148ex 401 . . . . . . 7 (𝐴𝑉 → ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
150149exlimdv 2028 . . . . . 6 (𝐴𝑉 → (∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
151128, 150impbid2 217 . . . . 5 (𝐴𝑉 → ((𝑦 ∈ On ∧ 𝑦𝐴) ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
15220, 151syl5bb 274 . . . 4 (𝐴𝑉 → (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
153152abbi2dv 2885 . . 3 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1541rneqi 5520 . . . 4 ran 𝐹 = ran {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
155 rnopab 5539 . . . 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 𝑟))}
156154, 155eqtri 2787 . . 3 ran 𝐹 = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
157153, 156syl6reqr 2818 . 2 (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴})
15815, 18, 1573pm3.2i 1438 1 (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107  wal 1650   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315   class class class wbr 4809  {copab 4871   I cid 5184   E cep 5189   Or wor 5197   Se wse 5234   We wwe 5235   × cxp 5275  dom cdm 5277  ran crn 5278  cres 5279  Ord word 5907  Oncon0 5908  Fun wfun 6062  wf 6064  1-1wf1 6065  1-1-ontowf1o 6067  cfv 6068   Isom wiso 6069  cen 8157  cdom 8158  OrdIsocoi 8621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-wrecs 7610  df-recs 7672  df-en 8161  df-dom 8162  df-oi 8622
This theorem is referenced by:  hartogslem2  8655  harwdom  8702
  Copyright terms: Public domain W3C validator