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

Theorem hartogslem1 8994
Description: Lemma for hartogs 8996. (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 5766 . . . 4 dom 𝐹 = dom {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
3 dmopab 5777 . . . 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 2841 . . 3 dom 𝐹 = {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
5 simp3 1130 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (dom 𝑟 × dom 𝑟))
6 simp1 1128 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → dom 𝑟𝐴)
7 xpss12 5563 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ dom 𝑟𝐴) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
86, 6, 7syl2anc 584 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
95, 8sstrd 3974 . . . . . . 7 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (𝐴 × 𝐴))
10 velpw 4543 . . . . . . 7 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
119, 10sylibr 235 . . . . . 6 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1211ad2antrr 722 . . . . 5 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1312exlimiv 1922 . . . 4 (∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1413abssi 4043 . . 3 {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝐴 × 𝐴)
154, 14eqsstri 3998 . 2 dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴)
16 funopab4 6385 . . 3 Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
171funeqi 6369 . . 3 (Fun 𝐹 ↔ Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1816, 17mpbir 232 . 2 Fun 𝐹
19 breq1 5060 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2019elrab 3677 . . . . 5 (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ (𝑦 ∈ On ∧ 𝑦𝐴))
21 f1f 6568 . . . . . . . . . . . . 13 (𝑓:𝑦1-1𝐴𝑓:𝑦𝐴)
2221adantl 482 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦𝐴)
2322frnd 6514 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ran 𝑓𝐴)
24 resss 5871 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ I
25 ssun2 4146 . . . . . . . . . . . . . 14 I ⊆ (𝑅 ∪ I )
2624, 25sstri 3973 . . . . . . . . . . . . 13 ( I ↾ ran 𝑓) ⊆ (𝑅 ∪ I )
27 idssxp 5909 . . . . . . . . . . . . 13 ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓)
2826, 27ssini 4205 . . . . . . . . . . . 12 ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))
2928a1i 11 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
30 inss2 4203 . . . . . . . . . . . 12 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
3130a1i 11 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))
3223, 29, 313jca 1120 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
33 eloni 6194 . . . . . . . . . . . . . 14 (𝑦 ∈ On → Ord 𝑦)
34 ordwe 6197 . . . . . . . . . . . . . 14 (Ord 𝑦 → E We 𝑦)
3533, 34syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ On → E We 𝑦)
3635adantr 481 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → E We 𝑦)
37 f1f1orn 6619 . . . . . . . . . . . . . . . 16 (𝑓:𝑦1-1𝐴𝑓:𝑦1-1-onto→ran 𝑓)
3837adantl 482 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦1-1-onto→ran 𝑓)
39 hartogslem.3 . . . . . . . . . . . . . . 15 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}
40 f1oiso 7093 . . . . . . . . . . . . . . 15 ((𝑓:𝑦1-1-onto→ran 𝑓𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
4138, 39, 40sylancl 586 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
42 isores2 7075 . . . . . . . . . . . . . 14 (𝑓 Isom E , 𝑅 (𝑦, ran 𝑓) ↔ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
4341, 42sylib 219 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
44 isowe 7091 . . . . . . . . . . . . 13 (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) → ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓))
4543, 44syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓))
4636, 45mpbid 233 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓)
47 weso 5539 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
4846, 47syl 17 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
49 inss2 4203 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
5049brel 5610 . . . . . . . . . . . . . . . . . 18 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥 → (𝑥 ∈ ran 𝑓𝑥 ∈ ran 𝑓))
5150simpld 495 . . . . . . . . . . . . . . . . 17 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥𝑥 ∈ ran 𝑓)
52 sonr 5489 . . . . . . . . . . . . . . . . 17 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓𝑥 ∈ ran 𝑓) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5348, 51, 52syl2an 595 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) ∧ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5453pm2.01da 795 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5554alrimiv 1919 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
56 intirr 5971 . . . . . . . . . . . . . 14 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
5755, 56sylibr 235 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅)
58 disj3 4399 . . . . . . . . . . . . 13 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
5957, 58sylib 219 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
60 weeq1 5536 . . . . . . . . . . . 12 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
6159, 60syl 17 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
6246, 61mpbid 233 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)
6333adantr 481 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → Ord 𝑦)
64 isoeq3 7061 . . . . . . . . . . . . . 14 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)))
6559, 64syl 17 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)))
6643, 65mpbid 233 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓))
67 vex 3495 . . . . . . . . . . . . . . 15 𝑓 ∈ V
6867rnex 7606 . . . . . . . . . . . . . 14 ran 𝑓 ∈ V
69 exse 5512 . . . . . . . . . . . . . 14 (ran 𝑓 ∈ V → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓)
7068, 69ax-mp 5 . . . . . . . . . . . . 13 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓
71 eqid 2818 . . . . . . . . . . . . . 14 OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)
7271oieu 8991 . . . . . . . . . . . . 13 ((((𝑅 ∩ (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 𝑓))))
7362, 70, 72sylancl 586 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((Ord 𝑦𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓)) ↔ (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))))
7463, 66, 73mpbi2and 708 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
7574simpld 495 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
7668, 68xpex 7465 . . . . . . . . . . . 12 (ran 𝑓 × ran 𝑓) ∈ V
7776inex2 5213 . . . . . . . . . . 11 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∈ V
78 sseq1 3989 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (ran 𝑓 × ran 𝑓) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
7930, 78mpbiri 259 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 ⊆ (ran 𝑓 × ran 𝑓))
80 dmss 5764 . . . . . . . . . . . . . . . . . 18 (𝑟 ⊆ (ran 𝑓 × ran 𝑓) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
8179, 80syl 17 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
82 dmxpid 5793 . . . . . . . . . . . . . . . . 17 dom (ran 𝑓 × ran 𝑓) = ran 𝑓
8381, 82sseqtrdi 4014 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ ran 𝑓)
84 dmresi 5914 . . . . . . . . . . . . . . . . 17 dom ( I ↾ ran 𝑓) = ran 𝑓
85 sseq2 3990 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ ran 𝑓) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
8628, 85mpbiri 259 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ ran 𝑓) ⊆ 𝑟)
87 dmss 5764 . . . . . . . . . . . . . . . . . 18 (( I ↾ ran 𝑓) ⊆ 𝑟 → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
8886, 87syl 17 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
8984, 88eqsstrrid 4013 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ran 𝑓 ⊆ dom 𝑟)
9083, 89eqssd 3981 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 = ran 𝑓)
9190sseq1d 3995 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟𝐴 ↔ ran 𝑓𝐴))
9290reseq2d 5846 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ dom 𝑟) = ( I ↾ ran 𝑓))
93 id 22 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
9492, 93sseq12d 3997 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ dom 𝑟) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
9590sqxpeqd 5580 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟 × dom 𝑟) = (ran 𝑓 × ran 𝑓))
9693, 95sseq12d 3997 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (dom 𝑟 × dom 𝑟) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
9791, 94, 963anbi123d 1427 . . . . . . . . . . . . 13 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ↔ (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))))
98 difeq1 4089 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
99 difun2 4425 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∪ I ) ∖ I ) = (𝑅 ∖ I )
10099ineq1i 4182 . . . . . . . . . . . . . . . . 17 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓))
101 indif1 4245 . . . . . . . . . . . . . . . . 17 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
102 indif1 4245 . . . . . . . . . . . . . . . . 17 ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
103100, 101, 1023eqtr3i 2849 . . . . . . . . . . . . . . . 16 (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
10498, 103syl6eq 2869 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
105 weeq1 5536 . . . . . . . . . . . . . . 15 ((𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟))
106104, 105syl 17 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟))
107 weeq2 5537 . . . . . . . . . . . . . . 15 (dom 𝑟 = ran 𝑓 → (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
10890, 107syl 17 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
109106, 108bitrd 280 . . . . . . . . . . . . 13 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((𝑟 ∖ I ) We dom 𝑟 ↔ ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓))
11097, 109anbi12d 630 . . . . . . . . . . . 12 (𝑟 = ((𝑅 ∪ 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 𝑓)))
111 oieq1 8964 . . . . . . . . . . . . . . . 16 ((𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟))
112104, 111syl 17 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟))
113 oieq2 8965 . . . . . . . . . . . . . . . 16 (dom 𝑟 = ran 𝑓 → OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
11490, 113syl 17 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
115112, 114eqtrd 2853 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
116115dmeqd 5767 . . . . . . . . . . . . 13 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
117116eqeq2d 2829 . . . . . . . . . . . 12 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟) ↔ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)))
118110, 117anbi12d 630 . . . . . . . . . . 11 (𝑟 = ((𝑅 ∪ 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 𝑓))))
11977, 118spcev 3604 . . . . . . . . . 10 ((((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 𝑟)))
12032, 62, 75, 119syl21anc 833 . . . . . . . . 9 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
121120ex 413 . . . . . . . 8 (𝑦 ∈ On → (𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
122121exlimdv 1925 . . . . . . 7 (𝑦 ∈ On → (∃𝑓 𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
123 brdomi 8508 . . . . . . 7 (𝑦𝐴 → ∃𝑓 𝑓:𝑦1-1𝐴)
124122, 123impel 506 . . . . . 6 ((𝑦 ∈ On ∧ 𝑦𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
125 simpr 485 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))
126 vex 3495 . . . . . . . . . . . . 13 𝑟 ∈ V
127126dmex 7605 . . . . . . . . . . . 12 dom 𝑟 ∈ V
128 eqid 2818 . . . . . . . . . . . . 13 OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso((𝑟 ∖ I ), dom 𝑟)
129128oion 8988 . . . . . . . . . . . 12 (dom 𝑟 ∈ V → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On)
130127, 129ax-mp 5 . . . . . . . . . . 11 dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On
131125, 130syl6eqel 2918 . . . . . . . . . 10 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ∈ On)
132131adantl 482 . . . . . . . . 9 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ∈ On)
133 simplr 765 . . . . . . . . . . . 12 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑟 ∖ I ) We dom 𝑟)
134128oien 8990 . . . . . . . . . . . 12 ((dom 𝑟 ∈ V ∧ (𝑟 ∖ I ) We dom 𝑟) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟)
135127, 133, 134sylancr 587 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ≈ dom 𝑟)
136125, 135eqbrtrd 5079 . . . . . . . . . 10 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ≈ dom 𝑟)
137 ssdomg 8543 . . . . . . . . . . 11 (𝐴𝑉 → (dom 𝑟𝐴 → dom 𝑟𝐴))
138 simpll1 1204 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom 𝑟𝐴)
139137, 138impel 506 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → dom 𝑟𝐴)
140 endomtr 8555 . . . . . . . . . 10 ((𝑦 ≈ dom 𝑟 ∧ dom 𝑟𝐴) → 𝑦𝐴)
141136, 139, 140syl2an2 682 . . . . . . . . 9 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦𝐴)
142132, 141jca 512 . . . . . . . 8 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → (𝑦 ∈ On ∧ 𝑦𝐴))
143142ex 413 . . . . . . 7 (𝐴𝑉 → ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
144143exlimdv 1925 . . . . . 6 (𝐴𝑉 → (∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
145124, 144impbid2 227 . . . . 5 (𝐴𝑉 → ((𝑦 ∈ On ∧ 𝑦𝐴) ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
14620, 145syl5bb 284 . . . 4 (𝐴𝑉 → (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
147146abbi2dv 2947 . . 3 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1481rneqi 5800 . . . 4 ran 𝐹 = ran {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
149 rnopab 5819 . . . 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 𝑟))}
150148, 149eqtri 2841 . . 3 ran 𝐹 = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
151147, 150syl6reqr 2872 . 2 (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴})
15215, 18, 1513pm3.2i 1331 1 (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079  wal 1526   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wrex 3136  {crab 3139  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535   class class class wbr 5057  {copab 5119   I cid 5452   E cep 5457   Or wor 5466   Se wse 5505   We wwe 5506   × cxp 5546  dom cdm 5548  ran crn 5549  cres 5550  Ord word 6183  Oncon0 6184  Fun wfun 6342  wf 6344  1-1wf1 6345  1-1-ontowf1o 6347  cfv 6348   Isom wiso 6349  cen 8494  cdom 8495  OrdIsocoi 8961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-wrecs 7936  df-recs 7997  df-en 8498  df-dom 8499  df-oi 8962
This theorem is referenced by:  hartogslem2  8995  harwdom  9042
  Copyright terms: Public domain W3C validator