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

Theorem hartogslem1 8330
Description: Lemma for hartogs 8332. (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 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 𝑟))}
42, 3eqtri 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 𝑟) ⊆ (𝐴 × 𝐴))
86, 6, 7syl2anc 691 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
95, 8sstrd 3578 . . . . . . 7 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (𝐴 × 𝐴))
10 selpw 4115 . . . . . . 7 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
119, 10sylibr 223 . . . . . 6 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1211ad2antrr 758 . . . . 5 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1312exlimiv 1845 . . . 4 (∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1413abssi 3640 . . 3 {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝐴 × 𝐴)
154, 14eqsstri 3598 . 2 dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴)
16 funopab4 5839 . . 3 Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
171funeqi 5824 . . 3 (Fun 𝐹 ↔ Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1816, 17mpbir 220 . 2 Fun 𝐹
19 breq1 4586 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2019elrab 3331 . . . . 5 (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ (𝑦 ∈ On ∧ 𝑦𝐴))
21 brdomi 7852 . . . . . . 7 (𝑦𝐴 → ∃𝑓 𝑓:𝑦1-1𝐴)
22 f1f 6014 . . . . . . . . . . . . . 14 (𝑓:𝑦1-1𝐴𝑓:𝑦𝐴)
2322adantl 481 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦𝐴)
24 frn 5966 . . . . . . . . . . . . 13 (𝑓:𝑦𝐴 → ran 𝑓𝐴)
2523, 24syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ran 𝑓𝐴)
26 resss 5342 . . . . . . . . . . . . . . 15 ( I ↾ ran 𝑓) ⊆ I
27 ssun2 3739 . . . . . . . . . . . . . . 15 I ⊆ (𝑅 ∪ I )
2826, 27sstri 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 𝑓))
3229, 30, 31mp2b 10 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓)
3328, 32ssini 3798 . . . . . . . . . . . . 13 ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))
3433a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
35 inss2 3796 . . . . . . . . . . . . 13 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
3635a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))
3725, 34, 363jca 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 𝑦)
4038, 39syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ On → E We 𝑦)
4140adantr 480 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → E We 𝑦)
42 f1f1orn 6061 . . . . . . . . . . . . . . . . 17 (𝑓:𝑦1-1𝐴𝑓:𝑦1-1-onto→ran 𝑓)
4342adantl 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 𝑓))
4643, 44, 45sylancl 693 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
47 isores2 6483 . . . . . . . . . . . . . . 15 (𝑓 Isom E , 𝑅 (𝑦, ran 𝑓) ↔ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
4846, 47sylib 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 𝑓))
5048, 49syl 17 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓))
5141, 50mpbid 221 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓)
52 weso 5029 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
5351, 52syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
54 inss2 3796 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
5554brel 5090 . . . . . . . . . . . . . . . . . . 19 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥 → (𝑥 ∈ ran 𝑓𝑥 ∈ ran 𝑓))
5655simpld 474 . . . . . . . . . . . . . . . . . 18 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥𝑥 ∈ ran 𝑓)
57 sonr 4980 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓𝑥 ∈ ran 𝑓) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5853, 56, 57syl2an 493 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) ∧ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5958pm2.01da 457 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
6059alrimiv 1842 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
61 intirr 5433 . . . . . . . . . . . . . . 15 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
6260, 61sylibr 223 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅)
63 disj3 3973 . . . . . . . . . . . . . 14 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
6462, 63sylib 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 𝑓))
6664, 65syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
6751, 66mpbid 221 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)
6838adantr 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 𝑓)))
7064, 69syl 17 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)))
7148, 70mpbid 221 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓))
72 vex 3176 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
7372rnex 6992 . . . . . . . . . . . . . . 15 ran 𝑓 ∈ V
74 exse 5002 . . . . . . . . . . . . . . 15 (ran 𝑓 ∈ V → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓)
7573, 74ax-mp 5 . . . . . . . . . . . . . 14 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓
76 eqid 2610 . . . . . . . . . . . . . . 15 OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)
7776oieu 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 𝑓))))
7867, 75, 77sylancl 693 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((Ord 𝑦𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)) ↔ (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))))
7968, 71, 78mpbi2and 958 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
8079simpld 474 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
8173, 73xpex 6860 . . . . . . . . . . . . 13 (ran 𝑓 × ran 𝑓) ∈ V
8281inex2 4728 . . . . . . . . . . . 12 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∈ V
83 sseq1 3589 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (ran 𝑓 × ran 𝑓) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
8435, 83mpbiri 247 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 ⊆ (ran 𝑓 × ran 𝑓))
85 dmss 5245 . . . . . . . . . . . . . . . . . . 19 (𝑟 ⊆ (ran 𝑓 × ran 𝑓) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
8684, 85syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
87 dmxpid 5266 . . . . . . . . . . . . . . . . . 18 dom (ran 𝑓 × ran 𝑓) = ran 𝑓
8886, 87syl6sseq 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 𝑓))))
9133, 90mpbiri 247 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ ran 𝑓) ⊆ 𝑟)
92 dmss 5245 . . . . . . . . . . . . . . . . . . 19 (( I ↾ ran 𝑓) ⊆ 𝑟 → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9391, 92syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9489, 93syl5eqssr 3613 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ran 𝑓 ⊆ dom 𝑟)
9588, 94eqssd 3585 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 = ran 𝑓)
9695sseq1d 3595 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟𝐴 ↔ ran 𝑓𝐴))
9795reseq2d 5317 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ dom 𝑟) = ( I ↾ ran 𝑓))
98 id 22 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
9997, 98sseq12d 3597 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ dom 𝑟) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
10095sqxpeqd 5065 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟 × dom 𝑟) = (ran 𝑓 × ran 𝑓))
10198, 100sseq12d 3597 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (dom 𝑟 × dom 𝑟) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
10296, 99, 1013anbi123d 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 )
105104ineq1i 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 )
108105, 106, 1073eqtr3i 2640 . . . . . . . . . . . . . . . . 17 (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
109103, 108syl6eq 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 𝑟))
111109, 110syl 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 𝑓))
11395, 112syl 17 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
114111, 113bitrd 267 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
115102, 114anbi12d 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 𝑟))
117109, 116syl 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 𝑓))
11995, 118syl 17 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
120117, 119eqtrd 2644 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
121120dmeqd 5248 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
122121eqeq2d 2620 . . . . . . . . . . . . 13 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟) ↔ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
123115, 122anbi12d 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 𝑓))))
12482, 123spcev 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 𝑟)))
12537, 67, 80, 124syl21anc 1317 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
126125ex 449 . . . . . . . . 9 (𝑦 ∈ On → (𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
127126exlimdv 1848 . . . . . . . 8 (𝑦 ∈ On → (∃𝑓 𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
128127imp 444 . . . . . . 7 ((𝑦 ∈ On ∧ ∃𝑓 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
12921, 128sylan2 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
132131dmex 6991 . . . . . . . . . . . 12 dom 𝑟 ∈ V
133 eqid 2610 . . . . . . . . . . . . 13 OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso((𝑟 ∖ I ), dom 𝑟)
134133oion 8324 . . . . . . . . . . . 12 (dom 𝑟 ∈ V → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On)
135132, 134ax-mp 5 . . . . . . . . . . 11 dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On
136130, 135syl6eqel 2696 . . . . . . . . . 10 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ∈ On)
137136adantl 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 𝑟)
139133oien 8326 . . . . . . . . . . . . 13 ((dom 𝑟 ∈ V ∧ (𝑟 ∖ I ) We dom 𝑟) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟)
140132, 138, 139sylancr 694 . . . . . . . . . . . 12 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟)
141130, 140eqbrtrd 4605 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ≈ dom 𝑟)
142141adantl 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 𝑟𝐴))
145144imp 444 . . . . . . . . . . 11 ((𝐴𝑉 ∧ dom 𝑟𝐴) → dom 𝑟𝐴)
146143, 145sylan2 490 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → dom 𝑟𝐴)
147 endomtr 7900 . . . . . . . . . 10 ((𝑦 ≈ dom 𝑟 ∧ dom 𝑟𝐴) → 𝑦𝐴)
148142, 146, 147syl2anc 691 . . . . . . . . 9 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦𝐴)
149137, 148jca 553 . . . . . . . 8 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → (𝑦 ∈ On ∧ 𝑦𝐴))
150149ex 449 . . . . . . 7 (𝐴𝑉 → ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
151150exlimdv 1848 . . . . . 6 (𝐴𝑉 → (∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
152129, 151impbid2 215 . . . . 5 (𝐴𝑉 → ((𝑦 ∈ On ∧ 𝑦𝐴) ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
15320, 152syl5bb 271 . . . 4 (𝐴𝑉 → (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
154153abbi2dv 2729 . . 3 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1551rneqi 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 𝑟))}
157155, 156eqtri 2632 . . 3 ran 𝐹 = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
158154, 157syl6reqr 2663 . 2 (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴})
15915, 18, 1583pm3.2i 1232 1 (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031  wal 1473   = wceq 1475  wex 1695  wcel 1977  {cab 2596  wrex 2897  {crab 2900  Vcvv 3173  cdif 3537  cun 3538  cin 3539  wss 3540  c0 3874  𝒫 cpw 4108   class class class wbr 4583  {copab 4642   E cep 4947   I cid 4948   Or wor 4958   Se wse 4995   We wwe 4996   × cxp 5036  dom cdm 5038  ran crn 5039  cres 5040  Ord word 5639  Oncon0 5640  Fun wfun 5798  wf 5800  1-1wf1 5801  1-1-ontowf1o 5803  cfv 5804   Isom wiso 5805  cen 7838  cdom 7839  OrdIsocoi 8297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-wrecs 7294  df-recs 7355  df-en 7842  df-dom 7843  df-oi 8298
This theorem is referenced by:  hartogslem2  8331  harwdom  8378
  Copyright terms: Public domain W3C validator