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

Theorem hartogslem1 8716
 Description: Lemma for hartogs 8718. (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 5557 . . . 4 dom 𝐹 = dom {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
3 dmopab 5567 . . . 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 2849 . . 3 dom 𝐹 = {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
5 simp3 1172 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (dom 𝑟 × dom 𝑟))
6 simp1 1170 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → dom 𝑟𝐴)
7 xpss12 5357 . . . . . . . . 9 ((dom 𝑟𝐴 ∧ dom 𝑟𝐴) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
86, 6, 7syl2anc 579 . . . . . . . 8 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → (dom 𝑟 × dom 𝑟) ⊆ (𝐴 × 𝐴))
95, 8sstrd 3837 . . . . . . 7 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ⊆ (𝐴 × 𝐴))
10 selpw 4385 . . . . . . 7 (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
119, 10sylibr 226 . . . . . 6 ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1211ad2antrr 717 . . . . 5 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1312exlimiv 2029 . . . 4 (∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
1413abssi 3902 . . 3 {𝑟 ∣ ∃𝑦(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝐴 × 𝐴)
154, 14eqsstri 3860 . 2 dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴)
16 funopab4 6160 . . 3 Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
171funeqi 6144 . . 3 (Fun 𝐹 ↔ Fun {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1816, 17mpbir 223 . 2 Fun 𝐹
19 breq1 4876 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2019elrab 3585 . . . . 5 (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ (𝑦 ∈ On ∧ 𝑦𝐴))
21 brdomi 8233 . . . . . . 7 (𝑦𝐴 → ∃𝑓 𝑓:𝑦1-1𝐴)
22 f1f 6338 . . . . . . . . . . . . . 14 (𝑓:𝑦1-1𝐴𝑓:𝑦𝐴)
2322adantl 475 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦𝐴)
2423frnd 6285 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ran 𝑓𝐴)
25 resss 5658 . . . . . . . . . . . . . . 15 ( I ↾ ran 𝑓) ⊆ I
26 ssun2 4004 . . . . . . . . . . . . . . 15 I ⊆ (𝑅 ∪ I )
2725, 26sstri 3836 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ (𝑅 ∪ I )
28 f1oi 6415 . . . . . . . . . . . . . . 15 ( I ↾ ran 𝑓):ran 𝑓1-1-onto→ran 𝑓
29 f1of 6378 . . . . . . . . . . . . . . 15 (( I ↾ ran 𝑓):ran 𝑓1-1-onto→ran 𝑓 → ( I ↾ ran 𝑓):ran 𝑓⟶ran 𝑓)
30 fssxp 6297 . . . . . . . . . . . . . . 15 (( I ↾ ran 𝑓):ran 𝑓⟶ran 𝑓 → ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓))
3128, 29, 30mp2b 10 . . . . . . . . . . . . . 14 ( I ↾ ran 𝑓) ⊆ (ran 𝑓 × ran 𝑓)
3227, 31ssini 4060 . . . . . . . . . . . . 13 ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))
3332a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
34 inss2 4058 . . . . . . . . . . . . 13 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
3534a1i 11 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))
3624, 33, 353jca 1162 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
37 eloni 5973 . . . . . . . . . . . . . . 15 (𝑦 ∈ On → Ord 𝑦)
38 ordwe 5976 . . . . . . . . . . . . . . 15 (Ord 𝑦 → E We 𝑦)
3937, 38syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ On → E We 𝑦)
4039adantr 474 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → E We 𝑦)
41 f1f1orn 6389 . . . . . . . . . . . . . . . . 17 (𝑓:𝑦1-1𝐴𝑓:𝑦1-1-onto→ran 𝑓)
4241adantl 475 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓:𝑦1-1-onto→ran 𝑓)
43 hartogslem.3 . . . . . . . . . . . . . . . 16 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}
44 f1oiso 6856 . . . . . . . . . . . . . . . 16 ((𝑓:𝑦1-1-onto→ran 𝑓𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤𝑦𝑧𝑦 ((𝑠 = (𝑓𝑤) ∧ 𝑡 = (𝑓𝑧)) ∧ 𝑤 E 𝑧)}) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
4542, 43, 44sylancl 580 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
46 isores2 6838 . . . . . . . . . . . . . . 15 (𝑓 Isom E , 𝑅 (𝑦, ran 𝑓) ↔ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
4745, 46sylib 210 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 × ran 𝑓))(𝑦, ran 𝑓))
48 isowe 6854 . . . . . . . . . . . . . 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 224 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓)
51 weso 5333 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) We ran 𝑓 → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) Or ran 𝑓)
53 inss2 4058 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)
5453brel 5401 . . . . . . . . . . . . . . . . . . 19 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥 → (𝑥 ∈ ran 𝑓𝑥 ∈ ran 𝑓))
5554simpld 490 . . . . . . . . . . . . . . . . . 18 (𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥𝑥 ∈ ran 𝑓)
56 sonr 5284 . . . . . . . . . . . . . . . . . 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 2026 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
60 intirr 5756 . . . . . . . . . . . . . . 15 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥(𝑅 ∩ (ran 𝑓 × ran 𝑓))𝑥)
6159, 60sylibr 226 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅)
62 disj3 4245 . . . . . . . . . . . . . 14 (((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∩ I ) = ∅ ↔ (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
6361, 62sylib 210 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → (𝑅 ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
64 weeq1 5330 . . . . . . . . . . . . 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 224 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) We ran 𝑓)
6737adantr 474 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → Ord 𝑦)
68 isoeq3 6824 . . . . . . . . . . . . . . 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 224 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )(𝑦, ran 𝑓))
71 vex 3417 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
7271rnex 7362 . . . . . . . . . . . . . . 15 ran 𝑓 ∈ V
73 exse 5306 . . . . . . . . . . . . . . 15 (ran 𝑓 ∈ V → ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓)
7472, 73ax-mp 5 . . . . . . . . . . . . . 14 ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) Se ran 𝑓
75 eqid 2825 . . . . . . . . . . . . . . 15 OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓)
7675oieu 8713 . . . . . . . . . . . . . 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 490 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
8072, 72xpex 7223 . . . . . . . . . . . . 13 (ran 𝑓 × ran 𝑓) ∈ V
8180inex2 5025 . . . . . . . . . . . 12 ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∈ V
82 sseq1 3851 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (ran 𝑓 × ran 𝑓) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
8334, 82mpbiri 250 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 ⊆ (ran 𝑓 × ran 𝑓))
84 dmss 5555 . . . . . . . . . . . . . . . . . . 19 (𝑟 ⊆ (ran 𝑓 × ran 𝑓) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
8583, 84syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ dom (ran 𝑓 × ran 𝑓))
86 dmxpid 5577 . . . . . . . . . . . . . . . . . 18 dom (ran 𝑓 × ran 𝑓) = ran 𝑓
8785, 86syl6sseq 3876 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 ⊆ ran 𝑓)
88 dmresi 5700 . . . . . . . . . . . . . . . . . 18 dom ( I ↾ ran 𝑓) = ran 𝑓
89 sseq2 3852 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ ran 𝑓) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
9032, 89mpbiri 250 . . . . . . . . . . . . . . . . . . 19 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ ran 𝑓) ⊆ 𝑟)
91 dmss 5555 . . . . . . . . . . . . . . . . . . 19 (( I ↾ ran 𝑓) ⊆ 𝑟 → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9290, 91syl 17 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom ( I ↾ ran 𝑓) ⊆ dom 𝑟)
9388, 92syl5eqssr 3875 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ran 𝑓 ⊆ dom 𝑟)
9487, 93eqssd 3844 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom 𝑟 = ran 𝑓)
9594sseq1d 3857 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟𝐴 ↔ ran 𝑓𝐴))
9694reseq2d 5629 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ( I ↾ dom 𝑟) = ( I ↾ ran 𝑓))
97 id 22 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → 𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)))
9896, 97sseq12d 3859 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (( I ↾ dom 𝑟) ⊆ 𝑟 ↔ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓))))
9994sqxpeqd 5374 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (dom 𝑟 × dom 𝑟) = (ran 𝑓 × ran 𝑓))
10097, 99sseq12d 3859 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ⊆ (dom 𝑟 × dom 𝑟) ↔ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓)))
10195, 98, 1003anbi123d 1564 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → ((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ↔ (ran 𝑓𝐴 ∧ ( I ↾ ran 𝑓) ⊆ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∧ ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ⊆ (ran 𝑓 × ran 𝑓))))
102 difeq1 3948 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
103 difun2 4271 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∪ I ) ∖ I ) = (𝑅 ∖ I )
104103ineq1i 4037 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓))
105 indif1 4101 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∪ I ) ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
106 indif1 4101 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∖ I ) ∩ (ran 𝑓 × ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
107104, 105, 1063eqtr3i 2857 . . . . . . . . . . . . . . . . 17 (((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I )
108102, 107syl6eq 2877 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → (𝑟 ∖ I ) = ((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ))
109 weeq1 5330 . . . . . . . . . . . . . . . 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 5331 . . . . . . . . . . . . . . . 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 271 . . . . . . . . . . . . . 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 8686 . . . . . . . . . . . . . . . . 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 8687 . . . . . . . . . . . . . . . . 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 2861 . . . . . . . . . . . . . . 15 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
120119dmeqd 5558 . . . . . . . . . . . . . 14 (𝑟 = ((𝑅 ∪ I ) ∩ (ran 𝑓 × ran 𝑓)) → dom OrdIso((𝑟 ∖ I ), dom 𝑟) = dom OrdIso(((𝑅 ∩ (ran 𝑓 × ran 𝑓)) ∖ I ), ran 𝑓))
121120eqeq2d 2835 . . . . . . . . . . . . 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 3517 . . . . . . . . . . 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 871 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦1-1𝐴) → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)))
125124ex 403 . . . . . . . . 9 (𝑦 ∈ On → (𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
126125exlimdv 2032 . . . . . . . 8 (𝑦 ∈ On → (∃𝑓 𝑓:𝑦1-1𝐴 → ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
127126imp 397 . . . . . . 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 479 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))
130 vex 3417 . . . . . . . . . . . . 13 𝑟 ∈ V
131130dmex 7361 . . . . . . . . . . . 12 dom 𝑟 ∈ V
132 eqid 2825 . . . . . . . . . . . . 13 OrdIso((𝑟 ∖ I ), dom 𝑟) = OrdIso((𝑟 ∖ I ), dom 𝑟)
133132oion 8710 . . . . . . . . . . . 12 (dom 𝑟 ∈ V → dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On)
134131, 133ax-mp 5 . . . . . . . . . . 11 dom OrdIso((𝑟 ∖ I ), dom 𝑟) ∈ On
135129, 134syl6eqel 2914 . . . . . . . . . 10 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ∈ On)
136135adantl 475 . . . . . . . . 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 8712 . . . . . . . . . . . . 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 4895 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → 𝑦 ≈ dom 𝑟)
141140adantl 475 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → 𝑦 ≈ dom 𝑟)
142 simpll1 1273 . . . . . . . . . . 11 ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → dom 𝑟𝐴)
143 ssdomg 8268 . . . . . . . . . . . 12 (𝐴𝑉 → (dom 𝑟𝐴 → dom 𝑟𝐴))
144143imp 397 . . . . . . . . . . 11 ((𝐴𝑉 ∧ dom 𝑟𝐴) → dom 𝑟𝐴)
145142, 144sylan2 586 . . . . . . . . . 10 ((𝐴𝑉 ∧ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))) → dom 𝑟𝐴)
146 endomtr 8280 . . . . . . . . . 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 403 . . . . . . 7 (𝐴𝑉 → ((((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
150149exlimdv 2032 . . . . . 6 (𝐴𝑉 → (∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟)) → (𝑦 ∈ On ∧ 𝑦𝐴)))
151128, 150impbid2 218 . . . . 5 (𝐴𝑉 → ((𝑦 ∈ On ∧ 𝑦𝐴) ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
15220, 151syl5bb 275 . . . 4 (𝐴𝑉 → (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))))
153152abbi2dv 2947 . . 3 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))})
1541rneqi 5584 . . . 4 ran 𝐹 = ran {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
155 rnopab 5603 . . . 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 2849 . . 3 ran 𝐹 = {𝑦 ∣ ∃𝑟(((dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}
157153, 156syl6reqr 2880 . 2 (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴})
15815, 18, 1573pm3.2i 1442 1 (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥𝐴}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1111  ∀wal 1654   = wceq 1656  ∃wex 1878   ∈ wcel 2164  {cab 2811  ∃wrex 3118  {crab 3121  Vcvv 3414   ∖ cdif 3795   ∪ cun 3796   ∩ cin 3797   ⊆ wss 3798  ∅c0 4144  𝒫 cpw 4378   class class class wbr 4873  {copab 4935   I cid 5249   E cep 5254   Or wor 5262   Se wse 5299   We wwe 5300   × cxp 5340  dom cdm 5342  ran crn 5343   ↾ cres 5344  Ord word 5962  Oncon0 5963  Fun wfun 6117  ⟶wf 6119  –1-1→wf1 6120  –1-1-onto→wf1o 6122  ‘cfv 6123   Isom wiso 6124   ≈ cen 8219   ≼ cdom 8220  OrdIsocoi 8683 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-wrecs 7672  df-recs 7734  df-en 8223  df-dom 8224  df-oi 8684 This theorem is referenced by:  hartogslem2  8717  harwdom  8764
 Copyright terms: Public domain W3C validator