MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hartogslem1 Structured version   Visualization version   GIF version
Theorem hartogslem1 9533
Description: Lemma for hartogs 9535. (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 5894 . . . 4 dom 𝐹 = dom {βŸ¨π‘Ÿ, π‘¦βŸ© ∣ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))}
3 dmopab 5905 . . . 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 2752 . . 3 dom 𝐹 = {π‘Ÿ ∣ βˆƒπ‘¦(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))}
5 simp3 1135 . . . . . . . 8 ((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) β†’ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ))
6 simp1 1133 . . . . . . . . 9 ((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) β†’ dom π‘Ÿ βŠ† 𝐴)
7 xpss12 5681 . . . . . . . . 9 ((dom π‘Ÿ βŠ† 𝐴 ∧ dom π‘Ÿ βŠ† 𝐴) β†’ (dom π‘Ÿ Γ— dom π‘Ÿ) βŠ† (𝐴 Γ— 𝐴))
86, 6, 7syl2anc 583 . . . . . . . 8 ((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) β†’ (dom π‘Ÿ Γ— dom π‘Ÿ) βŠ† (𝐴 Γ— 𝐴))
95, 8sstrd 3984 . . . . . . 7 ((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) β†’ π‘Ÿ βŠ† (𝐴 Γ— 𝐴))
10 velpw 4599 . . . . . . 7 (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐴) ↔ π‘Ÿ βŠ† (𝐴 Γ— 𝐴))
119, 10sylibr 233 . . . . . 6 ((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) β†’ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐴))
1211ad2antrr 723 . . . . 5 ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐴))
1312exlimiv 1925 . . . 4 (βˆƒπ‘¦(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐴))
1413abssi 4059 . . 3 {π‘Ÿ ∣ βˆƒπ‘¦(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))} βŠ† 𝒫 (𝐴 Γ— 𝐴)
154, 14eqsstri 4008 . 2 dom 𝐹 βŠ† 𝒫 (𝐴 Γ— 𝐴)
16 funopab4 6575 . . 3 Fun {βŸ¨π‘Ÿ, π‘¦βŸ© ∣ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))}
171funeqi 6559 . . 3 (Fun 𝐹 ↔ Fun {βŸ¨π‘Ÿ, π‘¦βŸ© ∣ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))})
1816, 17mpbir 230 . 2 Fun 𝐹
191rneqi 5926 . . . 4 ran 𝐹 = ran {βŸ¨π‘Ÿ, π‘¦βŸ© ∣ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))}
20 rnopab 5943 . . . 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 π‘Ÿ))}
2119, 20eqtri 2752 . . 3 ran 𝐹 = {𝑦 ∣ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))}
22 breq1 5141 . . . . . 6 (π‘₯ = 𝑦 β†’ (π‘₯ β‰Ό 𝐴 ↔ 𝑦 β‰Ό 𝐴))
2322elrab 3675 . . . . 5 (𝑦 ∈ {π‘₯ ∈ On ∣ π‘₯ β‰Ό 𝐴} ↔ (𝑦 ∈ On ∧ 𝑦 β‰Ό 𝐴))
24 f1f 6777 . . . . . . . . . . . . 13 (𝑓:𝑦–1-1→𝐴 β†’ 𝑓:π‘¦βŸΆπ΄)
2524adantl 481 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ 𝑓:π‘¦βŸΆπ΄)
2625frnd 6715 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ran 𝑓 βŠ† 𝐴)
27 resss 5996 . . . . . . . . . . . . . 14 ( I β†Ύ ran 𝑓) βŠ† I
28 ssun2 4165 . . . . . . . . . . . . . 14 I βŠ† (𝑅 βˆͺ I )
2927, 28sstri 3983 . . . . . . . . . . . . 13 ( I β†Ύ ran 𝑓) βŠ† (𝑅 βˆͺ I )
30 idssxp 6038 . . . . . . . . . . . . 13 ( I β†Ύ ran 𝑓) βŠ† (ran 𝑓 Γ— ran 𝑓)
3129, 30ssini 4223 . . . . . . . . . . . 12 ( I β†Ύ ran 𝑓) βŠ† ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓))
3231a1i 11 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ( I β†Ύ ran 𝑓) βŠ† ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)))
33 inss2 4221 . . . . . . . . . . . 12 ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βŠ† (ran 𝑓 Γ— ran 𝑓)
3433a1i 11 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βŠ† (ran 𝑓 Γ— ran 𝑓))
3526, 32, 343jca 1125 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ (ran 𝑓 βŠ† 𝐴 ∧ ( I β†Ύ ran 𝑓) βŠ† ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) ∧ ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βŠ† (ran 𝑓 Γ— ran 𝑓)))
36 eloni 6364 . . . . . . . . . . . . . 14 (𝑦 ∈ On β†’ Ord 𝑦)
37 ordwe 6367 . . . . . . . . . . . . . 14 (Ord 𝑦 β†’ E We 𝑦)
3836, 37syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ On β†’ E We 𝑦)
3938adantr 480 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ E We 𝑦)
40 f1f1orn 6834 . . . . . . . . . . . . . . . 16 (𝑓:𝑦–1-1→𝐴 β†’ 𝑓:𝑦–1-1-ontoβ†’ran 𝑓)
4140adantl 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ 𝑓:𝑦–1-1-ontoβ†’ran 𝑓)
42 hartogslem.3 . . . . . . . . . . . . . . 15 𝑅 = {βŸ¨π‘ , π‘‘βŸ© ∣ βˆƒπ‘€ ∈ 𝑦 βˆƒπ‘§ ∈ 𝑦 ((𝑠 = (π‘“β€˜π‘€) ∧ 𝑑 = (π‘“β€˜π‘§)) ∧ 𝑀 E 𝑧)}
43 f1oiso 7340 . . . . . . . . . . . . . . 15 ((𝑓:𝑦–1-1-ontoβ†’ran 𝑓 ∧ 𝑅 = {βŸ¨π‘ , π‘‘βŸ© ∣ βˆƒπ‘€ ∈ 𝑦 βˆƒπ‘§ ∈ 𝑦 ((𝑠 = (π‘“β€˜π‘€) ∧ 𝑑 = (π‘“β€˜π‘§)) ∧ 𝑀 E 𝑧)}) β†’ 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
4441, 42, 43sylancl 585 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ 𝑓 Isom E , 𝑅 (𝑦, ran 𝑓))
45 isores2 7322 . . . . . . . . . . . . . 14 (𝑓 Isom E , 𝑅 (𝑦, ran 𝑓) ↔ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))(𝑦, ran 𝑓))
4644, 45sylib 217 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ 𝑓 Isom E , (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))(𝑦, ran 𝑓))
47 isowe 7338 . . . . . . . . . . . . 13 (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))(𝑦, ran 𝑓) β†’ ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) We ran 𝑓))
4846, 47syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ( E We 𝑦 ↔ (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) We ran 𝑓))
4939, 48mpbid 231 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) We ran 𝑓)
50 weso 5657 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) We ran 𝑓 β†’ (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) Or ran 𝑓)
5149, 50syl 17 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) Or ran 𝑓)
52 inss2 4221 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βŠ† (ran 𝑓 Γ— ran 𝑓)
5352brel 5731 . . . . . . . . . . . . . . . . . 18 (π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯ β†’ (π‘₯ ∈ ran 𝑓 ∧ π‘₯ ∈ ran 𝑓))
5453simpld 494 . . . . . . . . . . . . . . . . 17 (π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯ β†’ π‘₯ ∈ ran 𝑓)
55 sonr 5601 . . . . . . . . . . . . . . . . 17 (((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) Or ran 𝑓 ∧ π‘₯ ∈ ran 𝑓) β†’ Β¬ π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯)
5651, 54, 55syl2an 595 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) ∧ π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯) β†’ Β¬ π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯)
5756pm2.01da 796 . . . . . . . . . . . . . . 15 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ Β¬ π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯)
5857alrimiv 1922 . . . . . . . . . . . . . 14 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ βˆ€π‘₯ Β¬ π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯)
59 intirr 6109 . . . . . . . . . . . . . 14 (((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) ∩ I ) = βˆ… ↔ βˆ€π‘₯ Β¬ π‘₯(𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))π‘₯)
6058, 59sylibr 233 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) ∩ I ) = βˆ…)
61 disj3 4445 . . . . . . . . . . . . 13 (((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) ∩ I ) = βˆ… ↔ (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ))
6260, 61sylib 217 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ))
63 weeq1 5654 . . . . . . . . . . . 12 ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) β†’ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We ran 𝑓))
6462, 63syl 17 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) We ran 𝑓 ↔ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We ran 𝑓))
6549, 64mpbid 231 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We ran 𝑓)
6636adantr 480 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ Ord 𝑦)
67 isoeq3 7308 . . . . . . . . . . . . . 14 ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) β†’ (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I )(𝑦, ran 𝑓)))
6862, 67syl 17 . . . . . . . . . . . . 13 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ (𝑓 Isom E , (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓))(𝑦, ran 𝑓) ↔ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I )(𝑦, ran 𝑓)))
6946, 68mpbid 231 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I )(𝑦, ran 𝑓))
70 vex 3470 . . . . . . . . . . . . . . 15 𝑓 ∈ V
7170rnex 7896 . . . . . . . . . . . . . 14 ran 𝑓 ∈ V
72 exse 5629 . . . . . . . . . . . . . 14 (ran 𝑓 ∈ V β†’ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) Se ran 𝑓)
7371, 72ax-mp 5 . . . . . . . . . . . . 13 ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) Se ran 𝑓
74 eqid 2724 . . . . . . . . . . . . . 14 OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓) = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓)
7574oieu 9530 . . . . . . . . . . . . 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 𝑓))))
7665, 73, 75sylancl 585 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ ((Ord 𝑦 ∧ 𝑓 Isom E , ( (𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I )(𝑦, ran 𝑓)) ↔ (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓))))
7766, 69, 76mpbi2and 709 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ (𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓) ∧ 𝑓 = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓)))
7877simpld 494 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓))
7971, 71xpex 7733 . . . . . . . . . . . 12 (ran 𝑓 Γ— ran 𝑓) ∈ V
8079inex2 5308 . . . . . . . . . . 11 ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) ∈ V
81 sseq1 3999 . . . . . . . . . . . . . . . . . . 19 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (π‘Ÿ βŠ† (ran 𝑓 Γ— ran 𝑓) ↔ ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βŠ† (ran 𝑓 Γ— ran 𝑓)))
8233, 81mpbiri 258 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ π‘Ÿ βŠ† (ran 𝑓 Γ— ran 𝑓))
83 dmss 5892 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ βŠ† (ran 𝑓 Γ— ran 𝑓) β†’ dom π‘Ÿ βŠ† dom (ran 𝑓 Γ— ran 𝑓))
8482, 83syl 17 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ dom π‘Ÿ βŠ† dom (ran 𝑓 Γ— ran 𝑓))
85 dmxpid 5919 . . . . . . . . . . . . . . . . 17 dom (ran 𝑓 Γ— ran 𝑓) = ran 𝑓
8684, 85sseqtrdi 4024 . . . . . . . . . . . . . . . 16 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ dom π‘Ÿ βŠ† ran 𝑓)
87 dmresi 6041 . . . . . . . . . . . . . . . . 17 dom ( I β†Ύ ran 𝑓) = ran 𝑓
88 sseq2 4000 . . . . . . . . . . . . . . . . . . 19 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (( I β†Ύ ran 𝑓) βŠ† π‘Ÿ ↔ ( I β†Ύ ran 𝑓) βŠ† ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓))))
8931, 88mpbiri 258 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ ( I β†Ύ ran 𝑓) βŠ† π‘Ÿ)
90 dmss 5892 . . . . . . . . . . . . . . . . . 18 (( I β†Ύ ran 𝑓) βŠ† π‘Ÿ β†’ dom ( I β†Ύ ran 𝑓) βŠ† dom π‘Ÿ)
9189, 90syl 17 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ dom ( I β†Ύ ran 𝑓) βŠ† dom π‘Ÿ)
9287, 91eqsstrrid 4023 . . . . . . . . . . . . . . . 16 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ ran 𝑓 βŠ† dom π‘Ÿ)
9386, 92eqssd 3991 . . . . . . . . . . . . . . 15 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ dom π‘Ÿ = ran 𝑓)
9493sseq1d 4005 . . . . . . . . . . . . . 14 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (dom π‘Ÿ βŠ† 𝐴 ↔ ran 𝑓 βŠ† 𝐴))
9593reseq2d 5971 . . . . . . . . . . . . . . 15 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ ( I β†Ύ dom π‘Ÿ) = ( I β†Ύ ran 𝑓))
96 id 22 . . . . . . . . . . . . . . 15 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)))
9795, 96sseq12d 4007 . . . . . . . . . . . . . 14 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ↔ ( I β†Ύ ran 𝑓) βŠ† ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓))))
9893sqxpeqd 5698 . . . . . . . . . . . . . . 15 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (dom π‘Ÿ Γ— dom π‘Ÿ) = (ran 𝑓 Γ— ran 𝑓))
9996, 98sseq12d 4007 . . . . . . . . . . . . . 14 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ) ↔ ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βŠ† (ran 𝑓 Γ— ran 𝑓)))
10094, 97, 993anbi123d 1432 . . . . . . . . . . . . 13 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ ((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ↔ (ran 𝑓 βŠ† 𝐴 ∧ ( I β†Ύ ran 𝑓) βŠ† ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) ∧ ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βŠ† (ran 𝑓 Γ— ran 𝑓))))
101 difeq1 4107 . . . . . . . . . . . . . . . 16 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (π‘Ÿ βˆ– I ) = (((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ))
102 difun2 4472 . . . . . . . . . . . . . . . . . 18 ((𝑅 βˆͺ I ) βˆ– I ) = (𝑅 βˆ– I )
103102ineq1i 4200 . . . . . . . . . . . . . . . . 17 (((𝑅 βˆͺ I ) βˆ– I ) ∩ (ran 𝑓 Γ— ran 𝑓)) = ((𝑅 βˆ– I ) ∩ (ran 𝑓 Γ— ran 𝑓))
104 indif1 4263 . . . . . . . . . . . . . . . . 17 (((𝑅 βˆͺ I ) βˆ– I ) ∩ (ran 𝑓 Γ— ran 𝑓)) = (((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I )
105 indif1 4263 . . . . . . . . . . . . . . . . 17 ((𝑅 βˆ– I ) ∩ (ran 𝑓 Γ— ran 𝑓)) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I )
106103, 104, 1053eqtr3i 2760 . . . . . . . . . . . . . . . 16 (((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I )
107101, 106eqtrdi 2780 . . . . . . . . . . . . . . 15 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (π‘Ÿ βˆ– I ) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ))
108 weeq1 5654 . . . . . . . . . . . . . . 15 ((π‘Ÿ βˆ– I ) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) β†’ ((π‘Ÿ βˆ– I ) We dom π‘Ÿ ↔ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We dom π‘Ÿ))
109107, 108syl 17 . . . . . . . . . . . . . 14 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ ((π‘Ÿ βˆ– I ) We dom π‘Ÿ ↔ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We dom π‘Ÿ))
110 weeq2 5655 . . . . . . . . . . . . . . 15 (dom π‘Ÿ = ran 𝑓 β†’ (((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We dom π‘Ÿ ↔ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We ran 𝑓))
11193, 110syl 17 . . . . . . . . . . . . . 14 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We dom π‘Ÿ ↔ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We ran 𝑓))
112109, 111bitrd 279 . . . . . . . . . . . . 13 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ ((π‘Ÿ βˆ– I ) We dom π‘Ÿ ↔ ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) We ran 𝑓))
113100, 112anbi12d 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 𝑓)))
114 oieq1 9503 . . . . . . . . . . . . . . . 16 ((π‘Ÿ βˆ– I ) = ((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ) β†’ OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), dom π‘Ÿ))
115107, 114syl 17 . . . . . . . . . . . . . . 15 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), dom π‘Ÿ))
116 oieq2 9504 . . . . . . . . . . . . . . . 16 (dom π‘Ÿ = ran 𝑓 β†’ OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), dom π‘Ÿ) = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓))
11793, 116syl 17 . . . . . . . . . . . . . . 15 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), dom π‘Ÿ) = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓))
118115, 117eqtrd 2764 . . . . . . . . . . . . . 14 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) = OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓))
119118dmeqd 5895 . . . . . . . . . . . . 13 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) = dom OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓))
120119eqeq2d 2735 . . . . . . . . . . . 12 (π‘Ÿ = ((𝑅 βˆͺ I ) ∩ (ran 𝑓 Γ— ran 𝑓)) β†’ (𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) ↔ 𝑦 = dom OrdIso(((𝑅 ∩ (ran 𝑓 Γ— ran 𝑓)) βˆ– I ), ran 𝑓)))
121113, 120anbi12d 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 𝑓))))
12280, 121spcev 3588 . . . . . . . . . 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 π‘Ÿ)))
12335, 65, 78, 122syl21anc 835 . . . . . . . . 9 ((𝑦 ∈ On ∧ 𝑓:𝑦–1-1→𝐴) β†’ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)))
124123ex 412 . . . . . . . 8 (𝑦 ∈ On β†’ (𝑓:𝑦–1-1→𝐴 β†’ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))))
125124exlimdv 1928 . . . . . . 7 (𝑦 ∈ On β†’ (βˆƒπ‘“ 𝑓:𝑦–1-1→𝐴 β†’ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))))
126 brdomi 8950 . . . . . . 7 (𝑦 β‰Ό 𝐴 β†’ βˆƒπ‘“ 𝑓:𝑦–1-1→𝐴)
127125, 126impel 505 . . . . . 6 ((𝑦 ∈ On ∧ 𝑦 β‰Ό 𝐴) β†’ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)))
128 simpr 484 . . . . . . . . . . 11 ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))
129 vex 3470 . . . . . . . . . . . . 13 π‘Ÿ ∈ V
130129dmex 7895 . . . . . . . . . . . 12 dom π‘Ÿ ∈ V
131 eqid 2724 . . . . . . . . . . . . 13 OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) = OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)
132131oion 9527 . . . . . . . . . . . 12 (dom π‘Ÿ ∈ V β†’ dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) ∈ On)
133130, 132ax-mp 5 . . . . . . . . . . 11 dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) ∈ On
134128, 133eqeltrdi 2833 . . . . . . . . . 10 ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ 𝑦 ∈ On)
135134adantl 481 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))) β†’ 𝑦 ∈ On)
136 simplr 766 . . . . . . . . . . . 12 ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ (π‘Ÿ βˆ– I ) We dom π‘Ÿ)
137131oien 9529 . . . . . . . . . . . 12 ((dom π‘Ÿ ∈ V ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) β†’ dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) β‰ˆ dom π‘Ÿ)
138130, 136, 137sylancr 586 . . . . . . . . . . 11 ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ) β‰ˆ dom π‘Ÿ)
139128, 138eqbrtrd 5160 . . . . . . . . . 10 ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ 𝑦 β‰ˆ dom π‘Ÿ)
140 ssdomg 8992 . . . . . . . . . . 11 (𝐴 ∈ 𝑉 β†’ (dom π‘Ÿ βŠ† 𝐴 β†’ dom π‘Ÿ β‰Ό 𝐴))
141 simpll1 1209 . . . . . . . . . . 11 ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ dom π‘Ÿ βŠ† 𝐴)
142140, 141impel 505 . . . . . . . . . 10 ((𝐴 ∈ 𝑉 ∧ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))) β†’ dom π‘Ÿ β‰Ό 𝐴)
143 endomtr 9004 . . . . . . . . . 10 ((𝑦 β‰ˆ dom π‘Ÿ ∧ dom π‘Ÿ β‰Ό 𝐴) β†’ 𝑦 β‰Ό 𝐴)
144139, 142, 143syl2an2 683 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))) β†’ 𝑦 β‰Ό 𝐴)
145135, 144jca 511 . . . . . . . 8 ((𝐴 ∈ 𝑉 ∧ (((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))) β†’ (𝑦 ∈ On ∧ 𝑦 β‰Ό 𝐴))
146145ex 412 . . . . . . 7 (𝐴 ∈ 𝑉 β†’ ((((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ (𝑦 ∈ On ∧ 𝑦 β‰Ό 𝐴)))
147146exlimdv 1928 . . . . . 6 (𝐴 ∈ 𝑉 β†’ (βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ)) β†’ (𝑦 ∈ On ∧ 𝑦 β‰Ό 𝐴)))
148127, 147impbid2 225 . . . . 5 (𝐴 ∈ 𝑉 β†’ ((𝑦 ∈ On ∧ 𝑦 β‰Ό 𝐴) ↔ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))))
14923, 148bitrid 283 . . . 4 (𝐴 ∈ 𝑉 β†’ (𝑦 ∈ {π‘₯ ∈ On ∣ π‘₯ β‰Ό 𝐴} ↔ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))))
150149eqabdv 2859 . . 3 (𝐴 ∈ 𝑉 β†’ {π‘₯ ∈ On ∣ π‘₯ β‰Ό 𝐴} = {𝑦 ∣ βˆƒπ‘Ÿ(((dom π‘Ÿ βŠ† 𝐴 ∧ ( I β†Ύ dom π‘Ÿ) βŠ† π‘Ÿ ∧ π‘Ÿ βŠ† (dom π‘Ÿ Γ— dom π‘Ÿ)) ∧ (π‘Ÿ βˆ– I ) We dom π‘Ÿ) ∧ 𝑦 = dom OrdIso((π‘Ÿ βˆ– I ), dom π‘Ÿ))})
15121, 150eqtr4id 2783 . 2 (𝐴 ∈ 𝑉 β†’ ran 𝐹 = {π‘₯ ∈ On ∣ π‘₯ β‰Ό 𝐴})
15215, 18, 1513pm3.2i 1336 1 (dom 𝐹 βŠ† 𝒫 (𝐴 Γ— 𝐴) ∧ Fun 𝐹 ∧ (𝐴 ∈ 𝑉 β†’ ran 𝐹 = {π‘₯ ∈ On ∣ π‘₯ β‰Ό 𝐴}))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084  βˆ€wal 1531   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  {cab 2701  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  π’« cpw 4594   class class class wbr 5138  {copab 5200   I cid 5563   E cep 5569   Or wor 5577   Se wse 5619   We wwe 5620   Γ— cxp 5664  dom cdm 5666  ran crn 5667   β†Ύ cres 5668  Ord word 6353  Oncon0 6354  Fun wfun 6527  βŸΆwf 6529  β€“1-1β†’wf1 6530  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533   Isom wiso 6534   β‰ˆ cen 8932   β‰Ό cdom 8933  OrdIsocoi 9500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-en 8936  df-dom 8937  df-oi 9501
This theorem is referenced by:  hartogslem2  9534  harwdom  9582
  Copyright terms: Public domain W3C validator