Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nofulllem5 Structured version   Visualization version   GIF version

Theorem nofulllem5 31105
 Description: Lemma for nofull (future) . Here, we introduce a new surreal number 𝑋. Eventually, we will show that either 𝑋 or a related surreal number has the required properties for the final theorem. We begin by calculating the domain of 𝑋. (Contributed by Scott Fenton, 1-May-2017.)
Hypotheses
Ref Expression
nofulllem5.1 𝑀 = {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}
nofulllem5.2 𝑆 = {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}
nofulllem5.3 𝑋 = 𝑆
Assertion
Ref Expression
nofulllem5 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → dom 𝑋 = 𝑀)
Distinct variable groups:   𝑥,𝐿,𝑦,𝑓,𝑔,,𝑎   𝑥,𝑅,𝑦,,𝑓,𝑔,𝑎   𝑥,𝑊,𝑦,𝑓,𝑔,,𝑎   𝑥,𝑉,𝑦,𝑓,𝑔,,𝑎   𝑀,𝑎,𝑓,𝑔,
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑓,𝑔,,𝑎)   𝑀(𝑥,𝑦)   𝑋(𝑥,𝑦,𝑓,𝑔,,𝑎)

Proof of Theorem nofulllem5
Dummy variables 𝑏 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nofulllem5.3 . . . 4 𝑋 = 𝑆
21dmeqi 5247 . . 3 dom 𝑋 = dom 𝑆
3 dmuni 5256 . . 3 dom 𝑆 = 𝑏𝑆 dom 𝑏
42, 3eqtri 2632 . 2 dom 𝑋 = 𝑏𝑆 dom 𝑏
5 iunss 4497 . . . . 5 ( 𝑏𝑆 dom 𝑏 𝑀 ↔ ∀𝑏𝑆 dom 𝑏 𝑀)
6 vex 3176 . . . . . . 7 𝑏 ∈ V
7 eqeq2 2621 . . . . . . . . . 10 (𝑓 = 𝑏 → ((𝑔𝑎) = 𝑓 ↔ (𝑔𝑎) = 𝑏))
8 eqeq2 2621 . . . . . . . . . 10 (𝑓 = 𝑏 → ((𝑎) = 𝑓 ↔ (𝑎) = 𝑏))
97, 8anbi12d 743 . . . . . . . . 9 (𝑓 = 𝑏 → (((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓) ↔ ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏)))
109rexbidv 3034 . . . . . . . 8 (𝑓 = 𝑏 → (∃𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓) ↔ ∃𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏)))
11102rexbidv 3039 . . . . . . 7 (𝑓 = 𝑏 → (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓) ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏)))
12 nofulllem5.2 . . . . . . 7 𝑆 = {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}
136, 11, 12elab2 3323 . . . . . 6 (𝑏𝑆 ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏))
14 inss1 3795 . . . . . . . . . . . 12 (𝑎 ∩ dom 𝑔) ⊆ 𝑎
15 elssuni 4403 . . . . . . . . . . . 12 (𝑎𝑀𝑎 𝑀)
1614, 15syl5ss 3579 . . . . . . . . . . 11 (𝑎𝑀 → (𝑎 ∩ dom 𝑔) ⊆ 𝑀)
17 dmres 5339 . . . . . . . . . . . . 13 dom (𝑔𝑎) = (𝑎 ∩ dom 𝑔)
18 dmeq 5246 . . . . . . . . . . . . 13 ((𝑔𝑎) = 𝑏 → dom (𝑔𝑎) = dom 𝑏)
1917, 18syl5eqr 2658 . . . . . . . . . . . 12 ((𝑔𝑎) = 𝑏 → (𝑎 ∩ dom 𝑔) = dom 𝑏)
2019sseq1d 3595 . . . . . . . . . . 11 ((𝑔𝑎) = 𝑏 → ((𝑎 ∩ dom 𝑔) ⊆ 𝑀 ↔ dom 𝑏 𝑀))
2116, 20syl5ibcom 234 . . . . . . . . . 10 (𝑎𝑀 → ((𝑔𝑎) = 𝑏 → dom 𝑏 𝑀))
2221adantrd 483 . . . . . . . . 9 (𝑎𝑀 → (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀))
2322rexlimiv 3009 . . . . . . . 8 (∃𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀)
2423a1i 11 . . . . . . 7 ((𝑔𝐿𝑅) → (∃𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀))
2524rexlimivv 3018 . . . . . 6 (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀)
2613, 25sylbi 206 . . . . 5 (𝑏𝑆 → dom 𝑏 𝑀)
275, 26mprgbir 2911 . . . 4 𝑏𝑆 dom 𝑏 𝑀
2827a1i 11 . . 3 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑏𝑆 dom 𝑏 𝑀)
29 nofulllem5.1 . . . . . . . . 9 𝑀 = {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}
3029nofulllem4 31104 . . . . . . . 8 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 ∈ On)
31 eloni 5650 . . . . . . . 8 (𝑀 ∈ On → Ord 𝑀)
3230, 31syl 17 . . . . . . 7 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → Ord 𝑀)
33 ordsucuniel 6916 . . . . . . 7 (Ord 𝑀 → (𝑗 𝑀 ↔ suc 𝑗𝑀))
3432, 33syl 17 . . . . . 6 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (𝑗 𝑀 ↔ suc 𝑗𝑀))
35 simpr 476 . . . . . . . 8 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → suc 𝑗𝑀)
36 onss 6882 . . . . . . . . . . . . 13 (𝑀 ∈ On → 𝑀 ⊆ On)
3730, 36syl 17 . . . . . . . . . . . 12 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 ⊆ On)
3837sselda 3568 . . . . . . . . . . 11 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → suc 𝑗 ∈ On)
39 ssrab2 3650 . . . . . . . . . . . . . . . . . . 19 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ⊆ On
40 onnmin 6895 . . . . . . . . . . . . . . . . . . 19 (({𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ⊆ On ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}) → ¬ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4139, 40mpan 702 . . . . . . . . . . . . . . . . . 18 (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} → ¬ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4241adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}) → ¬ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4329eleq2i 2680 . . . . . . . . . . . . . . . . 17 (suc 𝑗𝑀 ↔ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4442, 43sylnibr 318 . . . . . . . . . . . . . . . 16 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}) → ¬ suc 𝑗𝑀)
4544ex 449 . . . . . . . . . . . . . . 15 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} → ¬ suc 𝑗𝑀))
4645con2d 128 . . . . . . . . . . . . . 14 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (suc 𝑗𝑀 → ¬ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}))
4746imp 444 . . . . . . . . . . . . 13 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ¬ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
48 reseq2 5312 . . . . . . . . . . . . . . . . 17 (𝑎 = suc 𝑗 → (𝑥𝑎) = (𝑥 ↾ suc 𝑗))
49 reseq2 5312 . . . . . . . . . . . . . . . . 17 (𝑎 = suc 𝑗 → (𝑦𝑎) = (𝑦 ↾ suc 𝑗))
5048, 49neeq12d 2843 . . . . . . . . . . . . . . . 16 (𝑎 = suc 𝑗 → ((𝑥𝑎) ≠ (𝑦𝑎) ↔ (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
51502ralbidv 2972 . . . . . . . . . . . . . . 15 (𝑎 = suc 𝑗 → (∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎) ↔ ∀𝑥𝐿𝑦𝑅 (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
52 reseq1 5311 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑔 → (𝑥 ↾ suc 𝑗) = (𝑔 ↾ suc 𝑗))
5352neeq1d 2841 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑔 → ((𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ (𝑔 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
54 reseq1 5311 . . . . . . . . . . . . . . . . 17 (𝑦 = → (𝑦 ↾ suc 𝑗) = ( ↾ suc 𝑗))
5554neeq2d 2842 . . . . . . . . . . . . . . . 16 (𝑦 = → ((𝑔 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
5653, 55cbvral2v 3155 . . . . . . . . . . . . . . 15 (∀𝑥𝐿𝑦𝑅 (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
5751, 56syl6bb 275 . . . . . . . . . . . . . 14 (𝑎 = suc 𝑗 → (∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎) ↔ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
5857elrab 3331 . . . . . . . . . . . . 13 (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ↔ (suc 𝑗 ∈ On ∧ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
5947, 58sylnib 317 . . . . . . . . . . . 12 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ¬ (suc 𝑗 ∈ On ∧ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
60 imnan 437 . . . . . . . . . . . 12 ((suc 𝑗 ∈ On → ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)) ↔ ¬ (suc 𝑗 ∈ On ∧ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
6159, 60sylibr 223 . . . . . . . . . . 11 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → (suc 𝑗 ∈ On → ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
6238, 61mpd 15 . . . . . . . . . 10 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
63 df-ne 2782 . . . . . . . . . . . . . . 15 ((𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗) ↔ ¬ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗))
6463con2bii 346 . . . . . . . . . . . . . 14 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ¬ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
6564rexbii 3023 . . . . . . . . . . . . 13 (∃𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ∃𝑅 ¬ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
66 rexnal 2978 . . . . . . . . . . . . 13 (∃𝑅 ¬ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗) ↔ ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
6765, 66bitri 263 . . . . . . . . . . . 12 (∃𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
6867rexbii 3023 . . . . . . . . . . 11 (∃𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ∃𝑔𝐿 ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
69 rexnal 2978 . . . . . . . . . . 11 (∃𝑔𝐿 ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗) ↔ ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
7068, 69bitri 263 . . . . . . . . . 10 (∃𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
7162, 70sylibr 223 . . . . . . . . 9 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ∃𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗))
72 simp3 1056 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦)
73 breq1 4586 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑔 → (𝑥 <s 𝑦𝑔 <s 𝑦))
74 breq2 4587 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = → (𝑔 <s 𝑦𝑔 <s ))
7573, 74rspc2v 3293 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝐿𝑅) → (∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦𝑔 <s ))
7672, 75mpan9 485 . . . . . . . . . . . . . . . . . . 19 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (𝑔𝐿𝑅)) → 𝑔 <s )
7776adantrl 748 . . . . . . . . . . . . . . . . . 18 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → 𝑔 <s )
78 simp1l 1078 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝐿 No )
79 simprl 790 . . . . . . . . . . . . . . . . . . . 20 ((suc 𝑗𝑀 ∧ (𝑔𝐿𝑅)) → 𝑔𝐿)
80 ssel2 3563 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 No 𝑔𝐿) → 𝑔 No )
8178, 79, 80syl2an 493 . . . . . . . . . . . . . . . . . . 19 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → 𝑔 No )
82 sltirr 31069 . . . . . . . . . . . . . . . . . . 19 (𝑔 No → ¬ 𝑔 <s 𝑔)
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ¬ 𝑔 <s 𝑔)
84 breq2 4587 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → (𝑔 <s 𝑔𝑔 <s ))
8584biimprcd 239 . . . . . . . . . . . . . . . . . . 19 (𝑔 <s → (𝑔 = 𝑔 <s 𝑔))
8685con3d 147 . . . . . . . . . . . . . . . . . 18 (𝑔 <s → (¬ 𝑔 <s 𝑔 → ¬ 𝑔 = ))
8777, 83, 86sylc 63 . . . . . . . . . . . . . . . . 17 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ¬ 𝑔 = )
8887adantr 480 . . . . . . . . . . . . . . . 16 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → ¬ 𝑔 = )
89 ioran 510 . . . . . . . . . . . . . . . . 17 (¬ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ↔ (¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ))
90 simp2l 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑅 No )
91 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 𝑗𝑀 ∧ (𝑔𝐿𝑅)) → 𝑅)
92 ssel2 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 No 𝑅) → No )
9390, 91, 92syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → No )
9493adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → No )
95 nofun 31046 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( No → Fun )
96 funrel 5821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun → Rel )
9794, 95, 963syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → Rel )
9832adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord 𝑀)
99 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → suc 𝑗𝑀)
100 ordelon 5664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Ord 𝑀 ∧ suc 𝑗𝑀) → suc 𝑗 ∈ On)
10198, 99, 100syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → suc 𝑗 ∈ On)
102 sucelon 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ On ↔ suc 𝑗 ∈ On)
103101, 102sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → 𝑗 ∈ On)
104 eloni 5650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ On → Ord 𝑗)
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord 𝑗)
106 nodmord 31050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( No → Ord dom )
10793, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord dom )
108 ordtri2or 5739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑗 ∧ Ord dom ) → (𝑗 ∈ dom ∨ dom 𝑗))
109105, 107, 108syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (𝑗 ∈ dom ∨ dom 𝑗))
110109orcanai 950 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → dom 𝑗)
111 sssucid 5719 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 ⊆ suc 𝑗
112110, 111syl6ss 3580 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → dom ⊆ suc 𝑗)
113 relssres 5357 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel ∧ dom ⊆ suc 𝑗) → ( ↾ suc 𝑗) = )
11497, 112, 113syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → ( ↾ suc 𝑗) = )
115114ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (¬ 𝑗 ∈ dom → ( ↾ suc 𝑗) = ))
11681adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → 𝑔 No )
117 nofun 31046 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 No → Fun 𝑔)
118 funrel 5821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun 𝑔 → Rel 𝑔)
119116, 117, 1183syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → Rel 𝑔)
120 nodmord 31050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔 No → Ord dom 𝑔)
12181, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord dom 𝑔)
122 ordtri2or 5739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑗 ∧ Ord dom 𝑔) → (𝑗 ∈ dom 𝑔 ∨ dom 𝑔𝑗))
123105, 121, 122syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (𝑗 ∈ dom 𝑔 ∨ dom 𝑔𝑗))
124123orcanai 950 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → dom 𝑔𝑗)
125124, 111syl6ss 3580 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → dom 𝑔 ⊆ suc 𝑗)
126 relssres 5357 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑔 ∧ dom 𝑔 ⊆ suc 𝑗) → (𝑔 ↾ suc 𝑗) = 𝑔)
127119, 125, 126syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → (𝑔 ↾ suc 𝑗) = 𝑔)
128127ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (¬ 𝑗 ∈ dom 𝑔 → (𝑔 ↾ suc 𝑗) = 𝑔))
129115, 128anim12d 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((¬ 𝑗 ∈ dom ∧ ¬ 𝑗 ∈ dom 𝑔) → (( ↾ suc 𝑗) = ∧ (𝑔 ↾ suc 𝑗) = 𝑔)))
130129ancomsd 469 . . . . . . . . . . . . . . . . . . . 20 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → (( ↾ suc 𝑗) = ∧ (𝑔 ↾ suc 𝑗) = 𝑔)))
131 eqeq12 2623 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 ↾ suc 𝑗) = 𝑔 ∧ ( ↾ suc 𝑗) = ) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ 𝑔 = ))
132131biimpd 218 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔 ↾ suc 𝑗) = 𝑔 ∧ ( ↾ suc 𝑗) = ) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → 𝑔 = ))
133132ancoms 468 . . . . . . . . . . . . . . . . . . . 20 ((( ↾ suc 𝑗) = ∧ (𝑔 ↾ suc 𝑗) = 𝑔) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → 𝑔 = ))
134130, 133syl6 34 . . . . . . . . . . . . . . . . . . 19 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → 𝑔 = )))
135134com23 84 . . . . . . . . . . . . . . . . . 18 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → 𝑔 = )))
136135imp 444 . . . . . . . . . . . . . . . . 17 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → 𝑔 = ))
13789, 136syl5bi 231 . . . . . . . . . . . . . . . 16 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → (¬ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) → 𝑔 = ))
13888, 137mt3d 139 . . . . . . . . . . . . . . 15 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))
139138ex 449 . . . . . . . . . . . . . 14 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
140139anassrs 678 . . . . . . . . . . . . 13 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ (𝑔𝐿𝑅)) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
141140anassrs 678 . . . . . . . . . . . 12 ((((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ 𝑔𝐿) ∧ 𝑅) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
142141ancld 574 . . . . . . . . . . 11 ((((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ 𝑔𝐿) ∧ 𝑅) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
143142reximdva 3000 . . . . . . . . . 10 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ 𝑔𝐿) → (∃𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → ∃𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
144143reximdva 3000 . . . . . . . . 9 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → (∃𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → ∃𝑔𝐿𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
14571, 144mpd 15 . . . . . . . 8 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ∃𝑔𝐿𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
146 reseq2 5312 . . . . . . . . . . . . 13 (𝑎 = suc 𝑗 → (𝑔𝑎) = (𝑔 ↾ suc 𝑗))
147 reseq2 5312 . . . . . . . . . . . . 13 (𝑎 = suc 𝑗 → (𝑎) = ( ↾ suc 𝑗))
148146, 147eqeq12d 2625 . . . . . . . . . . . 12 (𝑎 = suc 𝑗 → ((𝑔𝑎) = (𝑎) ↔ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)))
149 eleq2 2677 . . . . . . . . . . . 12 (𝑎 = suc 𝑗 → (𝑗𝑎𝑗 ∈ suc 𝑗))
150148, 1493anbi13d 1393 . . . . . . . . . . 11 (𝑎 = suc 𝑗 → (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗 ∈ suc 𝑗)))
151 vex 3176 . . . . . . . . . . . . 13 𝑗 ∈ V
152151sucid 5721 . . . . . . . . . . . 12 𝑗 ∈ suc 𝑗
153 df-3an 1033 . . . . . . . . . . . 12 (((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗 ∈ suc 𝑗) ↔ (((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom )) ∧ 𝑗 ∈ suc 𝑗))
154152, 153mpbiran2 956 . . . . . . . . . . 11 (((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗 ∈ suc 𝑗) ↔ ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
155150, 154syl6bb 275 . . . . . . . . . 10 (𝑎 = suc 𝑗 → (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
1561552rexbidv 3039 . . . . . . . . 9 (𝑎 = suc 𝑗 → (∃𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
157156rspcev 3282 . . . . . . . 8 ((suc 𝑗𝑀 ∧ ∃𝑔𝐿𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))) → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
15835, 145, 157syl2anc 691 . . . . . . 7 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
159158ex 449 . . . . . 6 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (suc 𝑗𝑀 → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
16034, 159sylbid 229 . . . . 5 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (𝑗 𝑀 → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
161 eliun 4460 . . . . . 6 (𝑗 𝑏𝑆 dom 𝑏 ↔ ∃𝑏𝑆 𝑗 ∈ dom 𝑏)
16212rexeqi 3120 . . . . . 6 (∃𝑏𝑆 𝑗 ∈ dom 𝑏 ↔ ∃𝑏 ∈ {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}𝑗 ∈ dom 𝑏)
163 r19.41vv 3072 . . . . . . . . . 10 (∃𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
164163rexbii 3023 . . . . . . . . 9 (∃𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑔𝐿 (∃𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
165 r19.41v 3070 . . . . . . . . 9 (∃𝑔𝐿 (∃𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
166164, 165bitri 263 . . . . . . . 8 (∃𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
167166exbii 1764 . . . . . . 7 (∃𝑏𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏(∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
168 rexcom 3080 . . . . . . . . 9 (∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑎𝑀𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
169 rexcom 3080 . . . . . . . . . 10 (∃𝑎𝑀𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
170169rexbii 3023 . . . . . . . . 9 (∃𝑔𝐿𝑎𝑀𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
171168, 170bitri 263 . . . . . . . 8 (∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
172 vex 3176 . . . . . . . . . . . . . . . 16 ∈ V
173172resex 5363 . . . . . . . . . . . . . . 15 (𝑎) ∈ V
174 eqeq2 2621 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑎) → ((𝑔𝑎) = 𝑏 ↔ (𝑔𝑎) = (𝑎)))
175 dmeq 5246 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑎) → dom 𝑏 = dom (𝑎))
176175eleq2d 2673 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑎) → (𝑗 ∈ dom 𝑏𝑗 ∈ dom (𝑎)))
177174, 176anbi12d 743 . . . . . . . . . . . . . . 15 (𝑏 = (𝑎) → (((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏) ↔ ((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎))))
178173, 177ceqsexv 3215 . . . . . . . . . . . . . 14 (∃𝑏(𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎)))
179 an12 834 . . . . . . . . . . . . . . . 16 (((𝑎) = 𝑏 ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ((𝑔𝑎) = 𝑏 ∧ ((𝑎) = 𝑏𝑗 ∈ dom 𝑏)))
180 eqcom 2617 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑎) ↔ (𝑎) = 𝑏)
181180anbi1i 727 . . . . . . . . . . . . . . . 16 ((𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ((𝑎) = 𝑏 ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)))
182 anass 679 . . . . . . . . . . . . . . . 16 ((((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ((𝑔𝑎) = 𝑏 ∧ ((𝑎) = 𝑏𝑗 ∈ dom 𝑏)))
183179, 181, 1823bitr4i 291 . . . . . . . . . . . . . . 15 ((𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
184183exbii 1764 . . . . . . . . . . . . . 14 (∃𝑏(𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ∃𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
185 dmeq 5246 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑎) = (𝑎) → dom (𝑔𝑎) = dom (𝑎))
186185eleq2d 2673 . . . . . . . . . . . . . . . . . . 19 ((𝑔𝑎) = (𝑎) → (𝑗 ∈ dom (𝑔𝑎) ↔ 𝑗 ∈ dom (𝑎)))
187186orbi1d 735 . . . . . . . . . . . . . . . . . 18 ((𝑔𝑎) = (𝑎) → ((𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ (𝑗 ∈ dom (𝑎) ∨ 𝑗 ∈ dom (𝑎))))
188 oridm 535 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ dom (𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ 𝑗 ∈ dom (𝑎))
189187, 188syl6rbb 276 . . . . . . . . . . . . . . . . 17 ((𝑔𝑎) = (𝑎) → (𝑗 ∈ dom (𝑎) ↔ (𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎))))
190 incom 3767 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∩ dom 𝑔) = (dom 𝑔𝑎)
19117, 190eqtri 2632 . . . . . . . . . . . . . . . . . . . 20 dom (𝑔𝑎) = (dom 𝑔𝑎)
192191elin2 3763 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ dom (𝑔𝑎) ↔ (𝑗 ∈ dom 𝑔𝑗𝑎))
193 dmres 5339 . . . . . . . . . . . . . . . . . . . . 21 dom (𝑎) = (𝑎 ∩ dom )
194 incom 3767 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∩ dom ) = (dom 𝑎)
195193, 194eqtri 2632 . . . . . . . . . . . . . . . . . . . 20 dom (𝑎) = (dom 𝑎)
196195elin2 3763 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ dom (𝑎) ↔ (𝑗 ∈ dom 𝑗𝑎))
197192, 196orbi12i 542 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ ((𝑗 ∈ dom 𝑔𝑗𝑎) ∨ (𝑗 ∈ dom 𝑗𝑎)))
198 andir 908 . . . . . . . . . . . . . . . . . 18 (((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑗 ∈ dom 𝑔𝑗𝑎) ∨ (𝑗 ∈ dom 𝑗𝑎)))
199197, 198bitr4i 266 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
200189, 199syl6bb 275 . . . . . . . . . . . . . . . 16 ((𝑔𝑎) = (𝑎) → (𝑗 ∈ dom (𝑎) ↔ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
201200pm5.32i 667 . . . . . . . . . . . . . . 15 (((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎)) ↔ ((𝑔𝑎) = (𝑎) ∧ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
202 3anass 1035 . . . . . . . . . . . . . . 15 (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑔𝑎) = (𝑎) ∧ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
203201, 202bitr4i 266 . . . . . . . . . . . . . 14 (((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎)) ↔ ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
204178, 184, 2033bitr3ri 290 . . . . . . . . . . . . 13 (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
205204rexbii 3023 . . . . . . . . . . . 12 (∃𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑎𝑀𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
206 rexcom4 3198 . . . . . . . . . . . 12 (∃𝑎𝑀𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
207205, 206bitri 263 . . . . . . . . . . 11 (∃𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
208207rexbii 3023 . . . . . . . . . 10 (∃𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑅𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
209 rexcom4 3198 . . . . . . . . . 10 (∃𝑅𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
210208, 209bitri 263 . . . . . . . . 9 (∃𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
211210rexbii 3023 . . . . . . . 8 (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
212 rexcom4 3198 . . . . . . . 8 (∃𝑔𝐿𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
213171, 211, 2123bitri 285 . . . . . . 7 (∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
21411rexab 3336 . . . . . . 7 (∃𝑏 ∈ {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}𝑗 ∈ dom 𝑏 ↔ ∃𝑏(∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
215167, 213, 2143bitr4ri 292 . . . . . 6 (∃𝑏 ∈ {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}𝑗 ∈ dom 𝑏 ↔ ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
216161, 162, 2153bitri 285 . . . . 5 (𝑗 𝑏𝑆 dom 𝑏 ↔ ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
217160, 216syl6ibr 241 . . . 4 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (𝑗 𝑀𝑗 𝑏𝑆 dom 𝑏))
218217ssrdv 3574 . . 3 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 𝑏𝑆 dom 𝑏)
21928, 218eqssd 3585 . 2 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑏𝑆 dom 𝑏 = 𝑀)
2204, 219syl5eq 2656 1 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → dom 𝑋 = 𝑀)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ∩ cin 3539   ⊆ wss 3540  ∪ cuni 4372  ∩ cint 4410  ∪ ciun 4455   class class class wbr 4583  dom cdm 5038   ↾ cres 5040  Rel wrel 5043  Ord word 5639  Oncon0 5640  suc csuc 5642  Fun wfun 5798   No csur 31037
 Copyright terms: Public domain W3C validator