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

Theorem hartogslem1 8399
Description: Lemma for hartogs 8401. (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 5290 . . . 4 dom 𝐹 = dom {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
3 dmopab 5300 . . . 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 2643 . . 3 dom 𝐹 = {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
5 simp3 1061 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (dom 𝑟 × dom 𝑟))
6 simp1 1059 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → dom 𝑟𝐴)
7 xpss12 5191 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ dom 𝑟𝐴) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
86, 6, 7syl2anc 692 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
95, 8sstrd 3597 . . . . . . 7 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (𝐴 × 𝐴))
10 selpw 4142 . . . . . . 7 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
119, 10sylibr 224 . . . . . 6 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1211ad2antrr 761 . . . . 5 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1312exlimiv 1855 . . . 4 (∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1413abssi 3661 . . 3 {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝐴 × 𝐴)
154, 14eqsstri 3619 . 2 dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴)
16 funopab4 5888 . . 3 Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
171funeqi 5873 . . 3 (Fun 𝐹 ↔ Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1816, 17mpbir 221 . 2 Fun 𝐹
19 breq1 4621 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2019elrab 3350 . . . . 5 (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ (𝑦 ∈ On ∧ 𝑦𝐴))
21 brdomi 7918 . . . . . . 7 (𝑦𝐴 → ∃𝑓 𝑓:𝑦1-1𝐴)
22 f1f 6063 . . . . . . . . . . . . . 14 (𝑓:𝑦1-1𝐴𝑓:𝑦𝐴)
2322adantl 482 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦𝐴)
24 frn 6015 . . . . . . . . . . . . 13 (𝑓:𝑦𝐴 → ran 𝑓𝐴)
2523, 24syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ran 𝑓𝐴)
26 resss 5386 . . . . . . . . . . . . . . 15 ( I ↾ ran 𝑓) ⊆ I
27 ssun2 3760 . . . . . . . . . . . . . . 15 I ⊆ (𝑅 ∪ I )
2826, 27sstri 3596 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ (𝑅 ∪ I )
29 f1oi 6136 . . . . . . . . . . . . . . 15 ( I ↾ ran 𝑓):ran 𝑓1-1-onto→ran 𝑓
30 f1of 6099 . . . . . . . . . . . . . . 15 (( I ↾ ran 𝑓):ran 𝑓1-1-onto→ran 𝑓 → ( I ↾ ran 𝑓):ran 𝑓⟶ran 𝑓)
31 fssxp 6022 . . . . . . . . . . . . . . 15 (( I ↾ ran 𝑓):ran 𝑓⟶ran 𝑓 → ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓))
3229, 30, 31mp2b 10 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓)
3328, 32ssini 3819 . . . . . . . . . . . . 13 ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))
3433a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
35 inss2 3817 . . . . . . . . . . . . 13 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
3635a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))
3725, 34, 363jca 1240 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
38 eloni 5697 . . . . . . . . . . . . . . 15 (𝑦 ∈ On → Ord 𝑦)
39 ordwe 5700 . . . . . . . . . . . . . . 15 (Ord 𝑦 → E We 𝑦)
4038, 39syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ On → E We 𝑦)
4140adantr 481 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → E We 𝑦)
42 f1f1orn 6110 . . . . . . . . . . . . . . . . 17 (𝑓:𝑦1-1𝐴𝑓:𝑦1-1-onto→ran 𝑓)
4342adantl 482 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦1-1-onto→ran 𝑓)
44 hartogslem.3 . . . . . . . . . . . . . . . 16 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}
45 f1oiso 6561 . . . . . . . . . . . . . . . 16 ((𝑓:𝑦1-1-onto→ran 𝑓𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
4643, 44, 45sylancl 693 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
47 isores2 6543 . . . . . . . . . . . . . . 15 (𝑓 Isom E , 𝑅 (𝑦, ran 𝑓) ↔ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
4846, 47sylib 208 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
49 isowe 6559 . . . . . . . . . . . . . 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 222 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓)
52 weso 5070 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
5351, 52syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
54 inss2 3817 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
5554brel 5133 . . . . . . . . . . . . . . . . . . 19 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥 → (𝑥 ∈ ran 𝑓𝑥 ∈ ran 𝑓))
5655simpld 475 . . . . . . . . . . . . . . . . . 18 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥𝑥 ∈ ran 𝑓)
57 sonr 5021 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓𝑥 ∈ ran 𝑓) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5853, 56, 57syl2an 494 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) ∧ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5958pm2.01da 458 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
6059alrimiv 1852 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
61 intirr 5478 . . . . . . . . . . . . . . 15 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
6260, 61sylibr 224 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅)
63 disj3 3998 . . . . . . . . . . . . . 14 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
6462, 63sylib 208 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
65 weeq1 5067 . . . . . . . . . . . . 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 222 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)
6838adantr 481 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → Ord 𝑦)
69 isoeq3 6529 . . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓))
72 vex 3192 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
7372rnex 7054 . . . . . . . . . . . . . . 15 ran 𝑓 ∈ V
74 exse 5043 . . . . . . . . . . . . . . 15 (ran 𝑓 ∈ V → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓)
7573, 74ax-mp 5 . . . . . . . . . . . . . 14 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓
76 eqid 2621 . . . . . . . . . . . . . . 15 OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)
7776oieu 8396 . . . . . . . . . . . . . 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 955 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
8079simpld 475 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
8173, 73xpex 6922 . . . . . . . . . . . . 13 (ran 𝑓 × ran 𝑓) ∈ V
8281inex2 4765 . . . . . . . . . . . 12 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∈ V
83 sseq1 3610 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (ran 𝑓 × ran 𝑓) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
8435, 83mpbiri 248 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 ⊆ (ran 𝑓 × ran 𝑓))
85 dmss 5288 . . . . . . . . . . . . . . . . . . 19 (𝑟 ⊆ (ran 𝑓 × ran 𝑓) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
8684, 85syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
87 dmxpid 5310 . . . . . . . . . . . . . . . . . 18 dom (ran 𝑓 × ran 𝑓) = ran 𝑓
8886, 87syl6sseq 3635 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ ran 𝑓)
89 dmresi 5421 . . . . . . . . . . . . . . . . . 18 dom ( I ↾ ran 𝑓) = ran 𝑓
90 sseq2 3611 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ ran 𝑓) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
9133, 90mpbiri 248 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ ran 𝑓) ⊆ 𝑟)
92 dmss 5288 . . . . . . . . . . . . . . . . . . 19 (( I ↾ ran 𝑓) ⊆ 𝑟 → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9391, 92syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9489, 93syl5eqssr 3634 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ran 𝑓 ⊆ dom 𝑟)
9588, 94eqssd 3604 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 = ran 𝑓)
9695sseq1d 3616 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟𝐴 ↔ ran 𝑓𝐴))
9795reseq2d 5361 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ dom 𝑟) = ( I ↾ ran 𝑓))
98 id 22 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
9997, 98sseq12d 3618 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ dom 𝑟) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
10095sqxpeqd 5106 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟 × dom 𝑟) = (ran 𝑓 × ran 𝑓))
10198, 100sseq12d 3618 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (dom 𝑟 × dom 𝑟) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
10296, 99, 1013anbi123d 1396 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ↔ (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))))
103 difeq1 3704 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
104 difun2 4025 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∪ I ) ∖ I ) = (𝑅 ∖ I )
105104ineq1i 3793 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓))
106 indif1 3852 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
107 indif1 3852 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
108105, 106, 1073eqtr3i 2651 . . . . . . . . . . . . . . . . 17 (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
109103, 108syl6eq 2671 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
110 weeq1 5067 . . . . . . . . . . . . . . . 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 5068 . . . . . . . . . . . . . . . 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 268 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
115102, 114anbi12d 746 . . . . . . . . . . . . 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 8369 . . . . . . . . . . . . . . . . 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 8370 . . . . . . . . . . . . . . . . 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 2655 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
121120dmeqd 5291 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
122121eqeq2d 2631 . . . . . . . . . . . . 13 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟) ↔ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
123115, 122anbi12d 746 . . . . . . . . . . . 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 3289 . . . . . . . . . . 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 1322 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
126125ex 450 . . . . . . . . 9 (𝑦 ∈ On → (𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
127126exlimdv 1858 . . . . . . . 8 (𝑦 ∈ On → (∃𝑓 𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
128127imp 445 . . . . . . 7 ((𝑦 ∈ On ∧ ∃𝑓 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
12921, 128sylan2 491 . . . . . 6 ((𝑦 ∈ On ∧ 𝑦𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
130 simpr 477 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))
131 vex 3192 . . . . . . . . . . . . 13 𝑟 ∈ V
132131dmex 7053 . . . . . . . . . . . 12 dom 𝑟 ∈ V
133 eqid 2621 . . . . . . . . . . . . 13 OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso((𝑟 ∖ I ), dom 𝑟)
134133oion 8393 . . . . . . . . . . . 12 (dom 𝑟 ∈ V → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On)
135132, 134ax-mp 5 . . . . . . . . . . 11 dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On
136130, 135syl6eqel 2706 . . . . . . . . . 10 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ∈ On)
137136adantl 482 . . . . . . . . 9 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ∈ On)
138 simplr 791 . . . . . . . . . . . . 13 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑟 ∖ I ) We dom 𝑟)
139133oien 8395 . . . . . . . . . . . . 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 4640 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ≈ dom 𝑟)
142141adantl 482 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ≈ dom 𝑟)
143 simpll1 1098 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom 𝑟𝐴)
144 ssdomg 7953 . . . . . . . . . . . 12 (𝐴𝑉 → (dom 𝑟𝐴 → dom 𝑟𝐴))
145144imp 445 . . . . . . . . . . 11 ((𝐴𝑉 ∧ dom 𝑟𝐴) → dom 𝑟𝐴)
146143, 145sylan2 491 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → dom 𝑟𝐴)
147 endomtr 7966 . . . . . . . . . 10 ((𝑦 ≈ dom 𝑟 ∧ dom 𝑟𝐴) → 𝑦𝐴)
148142, 146, 147syl2anc 692 . . . . . . . . 9 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦𝐴)
149137, 148jca 554 . . . . . . . 8 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → (𝑦 ∈ On ∧ 𝑦𝐴))
150149ex 450 . . . . . . 7 (𝐴𝑉 → ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
151150exlimdv 1858 . . . . . 6 (𝐴𝑉 → (∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
152129, 151impbid2 216 . . . . 5 (𝐴𝑉 → ((𝑦 ∈ On ∧ 𝑦𝐴) ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
15320, 152syl5bb 272 . . . 4 (𝐴𝑉 → (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
154153abbi2dv 2739 . . 3 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1551rneqi 5317 . . . 4 ran 𝐹 = ran {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
156 rnopab 5335 . . . 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 2643 . . 3 ran 𝐹 = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
158154, 157syl6reqr 2674 . 2 (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴})
15915, 18, 1583pm3.2i 1237 1 (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036  wal 1478   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wrex 2908  {crab 2911  Vcvv 3189  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135   class class class wbr 4618  {copab 4677   E cep 4988   I cid 4989   Or wor 4999   Se wse 5036   We wwe 5037   × cxp 5077  dom cdm 5079  ran crn 5080  cres 5081  Ord word 5686  Oncon0 5687  Fun wfun 5846  wf 5848  1-1wf1 5849  1-1-ontowf1o 5851  cfv 5852   Isom wiso 5853  cen 7904  cdom 7905  OrdIsocoi 8366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-wrecs 7359  df-recs 7420  df-en 7908  df-dom 7909  df-oi 8367
This theorem is referenced by:  hartogslem2  8400  harwdom  8447
  Copyright terms: Public domain W3C validator