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

Theorem nofulllem5 30911
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 5234 . . 3 dom 𝑋 = dom 𝑆
3 dmuni 5243 . . 3 dom 𝑆 = 𝑏𝑆 dom 𝑏
42, 3eqtri 2631 . 2 dom 𝑋 = 𝑏𝑆 dom 𝑏
5 iunss 4491 . . . . 5 ( 𝑏𝑆 dom 𝑏 𝑀 ↔ ∀𝑏𝑆 dom 𝑏 𝑀)
6 vex 3175 . . . . . . 7 𝑏 ∈ V
7 eqeq2 2620 . . . . . . . . . 10 (𝑓 = 𝑏 → ((𝑔𝑎) = 𝑓 ↔ (𝑔𝑎) = 𝑏))
8 eqeq2 2620 . . . . . . . . . 10 (𝑓 = 𝑏 → ((𝑎) = 𝑓 ↔ (𝑎) = 𝑏))
97, 8anbi12d 742 . . . . . . . . 9 (𝑓 = 𝑏 → (((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓) ↔ ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏)))
109rexbidv 3033 . . . . . . . 8 (𝑓 = 𝑏 → (∃𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓) ↔ ∃𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏)))
11102rexbidv 3038 . . . . . . 7 (𝑓 = 𝑏 → (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓) ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏)))
12 nofulllem5.2 . . . . . . 7 𝑆 = {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}
136, 11, 12elab2 3322 . . . . . 6 (𝑏𝑆 ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏))
14 inss1 3794 . . . . . . . . . . . 12 (𝑎 ∩ dom 𝑔) ⊆ 𝑎
15 elssuni 4397 . . . . . . . . . . . 12 (𝑎𝑀𝑎 𝑀)
1614, 15syl5ss 3578 . . . . . . . . . . 11 (𝑎𝑀 → (𝑎 ∩ dom 𝑔) ⊆ 𝑀)
17 dmres 5326 . . . . . . . . . . . . 13 dom (𝑔𝑎) = (𝑎 ∩ dom 𝑔)
18 dmeq 5233 . . . . . . . . . . . . 13 ((𝑔𝑎) = 𝑏 → dom (𝑔𝑎) = dom 𝑏)
1917, 18syl5eqr 2657 . . . . . . . . . . . 12 ((𝑔𝑎) = 𝑏 → (𝑎 ∩ dom 𝑔) = dom 𝑏)
2019sseq1d 3594 . . . . . . . . . . 11 ((𝑔𝑎) = 𝑏 → ((𝑎 ∩ dom 𝑔) ⊆ 𝑀 ↔ dom 𝑏 𝑀))
2116, 20syl5ibcom 233 . . . . . . . . . 10 (𝑎𝑀 → ((𝑔𝑎) = 𝑏 → dom 𝑏 𝑀))
2221adantrd 482 . . . . . . . . 9 (𝑎𝑀 → (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀))
2322rexlimiv 3008 . . . . . . . 8 (∃𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀)
2423a1i 11 . . . . . . 7 ((𝑔𝐿𝑅) → (∃𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀))
2524rexlimivv 3017 . . . . . 6 (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) → dom 𝑏 𝑀)
2613, 25sylbi 205 . . . . 5 (𝑏𝑆 → dom 𝑏 𝑀)
275, 26mprgbir 2910 . . . 4 𝑏𝑆 dom 𝑏 𝑀
2827a1i 11 . . 3 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑏𝑆 dom 𝑏 𝑀)
29 nofulllem5.1 . . . . . . . . 9 𝑀 = {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}
3029nofulllem4 30910 . . . . . . . 8 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 ∈ On)
31 eloni 5636 . . . . . . . 8 (𝑀 ∈ On → Ord 𝑀)
3230, 31syl 17 . . . . . . 7 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → Ord 𝑀)
33 ordsucuniel 6893 . . . . . . 7 (Ord 𝑀 → (𝑗 𝑀 ↔ suc 𝑗𝑀))
3432, 33syl 17 . . . . . 6 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (𝑗 𝑀 ↔ suc 𝑗𝑀))
35 simpr 475 . . . . . . . 8 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → suc 𝑗𝑀)
36 onss 6859 . . . . . . . . . . . . 13 (𝑀 ∈ On → 𝑀 ⊆ On)
3730, 36syl 17 . . . . . . . . . . . 12 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 ⊆ On)
3837sselda 3567 . . . . . . . . . . 11 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → suc 𝑗 ∈ On)
39 ssrab2 3649 . . . . . . . . . . . . . . . . . . 19 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ⊆ On
40 onnmin 6872 . . . . . . . . . . . . . . . . . . 19 (({𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ⊆ On ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}) → ¬ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4139, 40mpan 701 . . . . . . . . . . . . . . . . . 18 (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} → ¬ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4241adantl 480 . . . . . . . . . . . . . . . . 17 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}) → ¬ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4329eleq2i 2679 . . . . . . . . . . . . . . . . 17 (suc 𝑗𝑀 ↔ suc 𝑗 {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
4442, 43sylnibr 317 . . . . . . . . . . . . . . . 16 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}) → ¬ suc 𝑗𝑀)
4544ex 448 . . . . . . . . . . . . . . 15 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} → ¬ suc 𝑗𝑀))
4645con2d 127 . . . . . . . . . . . . . 14 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (suc 𝑗𝑀 → ¬ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}))
4746imp 443 . . . . . . . . . . . . 13 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ¬ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)})
48 reseq2 5299 . . . . . . . . . . . . . . . . 17 (𝑎 = suc 𝑗 → (𝑥𝑎) = (𝑥 ↾ suc 𝑗))
49 reseq2 5299 . . . . . . . . . . . . . . . . 17 (𝑎 = suc 𝑗 → (𝑦𝑎) = (𝑦 ↾ suc 𝑗))
5048, 49neeq12d 2842 . . . . . . . . . . . . . . . 16 (𝑎 = suc 𝑗 → ((𝑥𝑎) ≠ (𝑦𝑎) ↔ (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
51502ralbidv 2971 . . . . . . . . . . . . . . 15 (𝑎 = suc 𝑗 → (∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎) ↔ ∀𝑥𝐿𝑦𝑅 (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
52 reseq1 5298 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑔 → (𝑥 ↾ suc 𝑗) = (𝑔 ↾ suc 𝑗))
5352neeq1d 2840 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑔 → ((𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ (𝑔 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
54 reseq1 5298 . . . . . . . . . . . . . . . . 17 (𝑦 = → (𝑦 ↾ suc 𝑗) = ( ↾ suc 𝑗))
5554neeq2d 2841 . . . . . . . . . . . . . . . 16 (𝑦 = → ((𝑔 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
5653, 55cbvral2v 3154 . . . . . . . . . . . . . . 15 (∀𝑥𝐿𝑦𝑅 (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
5751, 56syl6bb 274 . . . . . . . . . . . . . 14 (𝑎 = suc 𝑗 → (∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎) ↔ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
5857elrab 3330 . . . . . . . . . . . . 13 (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ↔ (suc 𝑗 ∈ On ∧ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
5947, 58sylnib 316 . . . . . . . . . . . 12 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ¬ (suc 𝑗 ∈ On ∧ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
60 imnan 436 . . . . . . . . . . . 12 ((suc 𝑗 ∈ On → ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)) ↔ ¬ (suc 𝑗 ∈ On ∧ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
6159, 60sylibr 222 . . . . . . . . . . 11 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → (suc 𝑗 ∈ On → ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗)))
6238, 61mpd 15 . . . . . . . . . 10 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
63 df-ne 2781 . . . . . . . . . . . . . . 15 ((𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗) ↔ ¬ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗))
6463con2bii 345 . . . . . . . . . . . . . 14 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ¬ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
6564rexbii 3022 . . . . . . . . . . . . 13 (∃𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ∃𝑅 ¬ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
66 rexnal 2977 . . . . . . . . . . . . 13 (∃𝑅 ¬ (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗) ↔ ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
6765, 66bitri 262 . . . . . . . . . . . 12 (∃𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
6867rexbii 3022 . . . . . . . . . . 11 (∃𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ∃𝑔𝐿 ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
69 rexnal 2977 . . . . . . . . . . 11 (∃𝑔𝐿 ¬ ∀𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗) ↔ ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
7068, 69bitri 262 . . . . . . . . . 10 (∃𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ ¬ ∀𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) ≠ ( ↾ suc 𝑗))
7162, 70sylibr 222 . . . . . . . . 9 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ∃𝑔𝐿𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗))
72 simp3 1055 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦)
73 breq1 4580 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑔 → (𝑥 <s 𝑦𝑔 <s 𝑦))
74 breq2 4581 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = → (𝑔 <s 𝑦𝑔 <s ))
7573, 74rspc2v 3292 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝐿𝑅) → (∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦𝑔 <s ))
7672, 75mpan9 484 . . . . . . . . . . . . . . . . . . 19 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (𝑔𝐿𝑅)) → 𝑔 <s )
7776adantrl 747 . . . . . . . . . . . . . . . . . 18 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → 𝑔 <s )
78 simp1l 1077 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝐿 No )
79 simprl 789 . . . . . . . . . . . . . . . . . . . 20 ((suc 𝑗𝑀 ∧ (𝑔𝐿𝑅)) → 𝑔𝐿)
80 ssel2 3562 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 No 𝑔𝐿) → 𝑔 No )
8178, 79, 80syl2an 492 . . . . . . . . . . . . . . . . . . 19 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → 𝑔 No )
82 sltirr 30875 . . . . . . . . . . . . . . . . . . 19 (𝑔 No → ¬ 𝑔 <s 𝑔)
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ¬ 𝑔 <s 𝑔)
84 breq2 4581 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → (𝑔 <s 𝑔𝑔 <s ))
8584biimprcd 238 . . . . . . . . . . . . . . . . . . 19 (𝑔 <s → (𝑔 = 𝑔 <s 𝑔))
8685con3d 146 . . . . . . . . . . . . . . . . . 18 (𝑔 <s → (¬ 𝑔 <s 𝑔 → ¬ 𝑔 = ))
8777, 83, 86sylc 62 . . . . . . . . . . . . . . . . 17 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ¬ 𝑔 = )
8887adantr 479 . . . . . . . . . . . . . . . 16 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → ¬ 𝑔 = )
89 ioran 509 . . . . . . . . . . . . . . . . 17 (¬ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ↔ (¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ))
90 simp2l 1079 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑅 No )
91 simprr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 𝑗𝑀 ∧ (𝑔𝐿𝑅)) → 𝑅)
92 ssel2 3562 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 No 𝑅) → No )
9390, 91, 92syl2an 492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → No )
9493adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → No )
95 nofun 30852 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( No → Fun )
96 funrel 5807 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun → Rel )
9794, 95, 963syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → Rel )
9832adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord 𝑀)
99 simprl 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → suc 𝑗𝑀)
100 ordelon 5650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Ord 𝑀 ∧ suc 𝑗𝑀) → suc 𝑗 ∈ On)
10198, 99, 100syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → suc 𝑗 ∈ On)
102 sucelon 6886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ On ↔ suc 𝑗 ∈ On)
103101, 102sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → 𝑗 ∈ On)
104 eloni 5636 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ On → Ord 𝑗)
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord 𝑗)
106 nodmord 30856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( No → Ord dom )
10793, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord dom )
108 ordtri2or 5725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑗 ∧ Ord dom ) → (𝑗 ∈ dom ∨ dom 𝑗))
109105, 107, 108syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (𝑗 ∈ dom ∨ dom 𝑗))
110109orcanai 949 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → dom 𝑗)
111 sssucid 5705 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 ⊆ suc 𝑗
112110, 111syl6ss 3579 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → dom ⊆ suc 𝑗)
113 relssres 5344 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel ∧ dom ⊆ suc 𝑗) → ( ↾ suc 𝑗) = )
11497, 112, 113syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom ) → ( ↾ suc 𝑗) = )
115114ex 448 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (¬ 𝑗 ∈ dom → ( ↾ suc 𝑗) = ))
11681adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → 𝑔 No )
117 nofun 30852 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 No → Fun 𝑔)
118 funrel 5807 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun 𝑔 → Rel 𝑔)
119116, 117, 1183syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → Rel 𝑔)
120 nodmord 30856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔 No → Ord dom 𝑔)
12181, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → Ord dom 𝑔)
122 ordtri2or 5725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑗 ∧ Ord dom 𝑔) → (𝑗 ∈ dom 𝑔 ∨ dom 𝑔𝑗))
123105, 121, 122syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (𝑗 ∈ dom 𝑔 ∨ dom 𝑔𝑗))
124123orcanai 949 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → dom 𝑔𝑗)
125124, 111syl6ss 3579 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → dom 𝑔 ⊆ suc 𝑗)
126 relssres 5344 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑔 ∧ dom 𝑔 ⊆ suc 𝑗) → (𝑔 ↾ suc 𝑗) = 𝑔)
127119, 125, 126syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → (𝑔 ↾ suc 𝑗) = 𝑔)
128127ex 448 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → (¬ 𝑗 ∈ dom 𝑔 → (𝑔 ↾ suc 𝑗) = 𝑔))
129115, 128anim12d 583 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((¬ 𝑗 ∈ dom ∧ ¬ 𝑗 ∈ dom 𝑔) → (( ↾ suc 𝑗) = ∧ (𝑔 ↾ suc 𝑗) = 𝑔)))
130129ancomsd 468 . . . . . . . . . . . . . . . . . . . 20 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → (( ↾ suc 𝑗) = ∧ (𝑔 ↾ suc 𝑗) = 𝑔)))
131 eqeq12 2622 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 ↾ suc 𝑗) = 𝑔 ∧ ( ↾ suc 𝑗) = ) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ↔ 𝑔 = ))
132131biimpd 217 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔 ↾ suc 𝑗) = 𝑔 ∧ ( ↾ suc 𝑗) = ) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → 𝑔 = ))
133132ancoms 467 . . . . . . . . . . . . . . . . . . . 20 ((( ↾ suc 𝑗) = ∧ (𝑔 ↾ suc 𝑗) = 𝑔) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → 𝑔 = ))
134130, 133syl6 34 . . . . . . . . . . . . . . . . . . 19 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → 𝑔 = )))
135134com23 83 . . . . . . . . . . . . . . . . . 18 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → 𝑔 = )))
136135imp 443 . . . . . . . . . . . . . . . . 17 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ) → 𝑔 = ))
13789, 136syl5bi 230 . . . . . . . . . . . . . . . 16 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → (¬ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) → 𝑔 = ))
13888, 137mt3d 138 . . . . . . . . . . . . . . 15 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) ∧ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))
139138ex 448 . . . . . . . . . . . . . 14 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗𝑀 ∧ (𝑔𝐿𝑅))) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
140139anassrs 677 . . . . . . . . . . . . 13 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ (𝑔𝐿𝑅)) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
141140anassrs 677 . . . . . . . . . . . 12 ((((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ 𝑔𝐿) ∧ 𝑅) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
142141ancld 573 . . . . . . . . . . 11 ((((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ 𝑔𝐿) ∧ 𝑅) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
143142reximdva 2999 . . . . . . . . . 10 (((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) ∧ 𝑔𝐿) → (∃𝑅 (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) → ∃𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
144143reximdva 2999 . . . . . . . . 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 5299 . . . . . . . . . . . . 13 (𝑎 = suc 𝑗 → (𝑔𝑎) = (𝑔 ↾ suc 𝑗))
147 reseq2 5299 . . . . . . . . . . . . 13 (𝑎 = suc 𝑗 → (𝑎) = ( ↾ suc 𝑗))
148146, 147eqeq12d 2624 . . . . . . . . . . . 12 (𝑎 = suc 𝑗 → ((𝑔𝑎) = (𝑎) ↔ (𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗)))
149 eleq2 2676 . . . . . . . . . . . 12 (𝑎 = suc 𝑗 → (𝑗𝑎𝑗 ∈ suc 𝑗))
150148, 1493anbi13d 1392 . . . . . . . . . . 11 (𝑎 = suc 𝑗 → (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗 ∈ suc 𝑗)))
151 vex 3175 . . . . . . . . . . . . 13 𝑗 ∈ V
152151sucid 5707 . . . . . . . . . . . 12 𝑗 ∈ suc 𝑗
153 df-3an 1032 . . . . . . . . . . . 12 (((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗 ∈ suc 𝑗) ↔ (((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom )) ∧ 𝑗 ∈ suc 𝑗))
154152, 153mpbiran2 955 . . . . . . . . . . 11 (((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗 ∈ suc 𝑗) ↔ ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom )))
155150, 154syl6bb 274 . . . . . . . . . 10 (𝑎 = suc 𝑗 → (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
1561552rexbidv 3038 . . . . . . . . 9 (𝑎 = suc 𝑗 → (∃𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))))
157156rspcev 3281 . . . . . . . 8 ((suc 𝑗𝑀 ∧ ∃𝑔𝐿𝑅 ((𝑔 ↾ suc 𝑗) = ( ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ))) → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
15835, 145, 157syl2anc 690 . . . . . . 7 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) ∧ suc 𝑗𝑀) → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
159158ex 448 . . . . . 6 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (suc 𝑗𝑀 → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
16034, 159sylbid 228 . . . . 5 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (𝑗 𝑀 → ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
161 eliun 4454 . . . . . 6 (𝑗 𝑏𝑆 dom 𝑏 ↔ ∃𝑏𝑆 𝑗 ∈ dom 𝑏)
16212rexeqi 3119 . . . . . 6 (∃𝑏𝑆 𝑗 ∈ dom 𝑏 ↔ ∃𝑏 ∈ {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}𝑗 ∈ dom 𝑏)
163 r19.41vv 3071 . . . . . . . . . 10 (∃𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
164163rexbii 3022 . . . . . . . . 9 (∃𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑔𝐿 (∃𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
165 r19.41v 3069 . . . . . . . . 9 (∃𝑔𝐿 (∃𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
166164, 165bitri 262 . . . . . . . 8 (∃𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
167166exbii 1763 . . . . . . 7 (∃𝑏𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏(∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
168 rexcom 3079 . . . . . . . . 9 (∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑎𝑀𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
169 rexcom 3079 . . . . . . . . . 10 (∃𝑎𝑀𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
170169rexbii 3022 . . . . . . . . 9 (∃𝑔𝐿𝑎𝑀𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
171168, 170bitri 262 . . . . . . . 8 (∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
172 vex 3175 . . . . . . . . . . . . . . . 16 ∈ V
173172resex 5350 . . . . . . . . . . . . . . 15 (𝑎) ∈ V
174 eqeq2 2620 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑎) → ((𝑔𝑎) = 𝑏 ↔ (𝑔𝑎) = (𝑎)))
175 dmeq 5233 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑎) → dom 𝑏 = dom (𝑎))
176175eleq2d 2672 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑎) → (𝑗 ∈ dom 𝑏𝑗 ∈ dom (𝑎)))
177174, 176anbi12d 742 . . . . . . . . . . . . . . 15 (𝑏 = (𝑎) → (((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏) ↔ ((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎))))
178173, 177ceqsexv 3214 . . . . . . . . . . . . . 14 (∃𝑏(𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎)))
179 an12 833 . . . . . . . . . . . . . . . 16 (((𝑎) = 𝑏 ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ((𝑔𝑎) = 𝑏 ∧ ((𝑎) = 𝑏𝑗 ∈ dom 𝑏)))
180 eqcom 2616 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑎) ↔ (𝑎) = 𝑏)
181180anbi1i 726 . . . . . . . . . . . . . . . 16 ((𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ((𝑎) = 𝑏 ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)))
182 anass 678 . . . . . . . . . . . . . . . 16 ((((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ((𝑔𝑎) = 𝑏 ∧ ((𝑎) = 𝑏𝑗 ∈ dom 𝑏)))
183179, 181, 1823bitr4i 290 . . . . . . . . . . . . . . 15 ((𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
184183exbii 1763 . . . . . . . . . . . . . 14 (∃𝑏(𝑏 = (𝑎) ∧ ((𝑔𝑎) = 𝑏𝑗 ∈ dom 𝑏)) ↔ ∃𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
185 dmeq 5233 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑎) = (𝑎) → dom (𝑔𝑎) = dom (𝑎))
186185eleq2d 2672 . . . . . . . . . . . . . . . . . . 19 ((𝑔𝑎) = (𝑎) → (𝑗 ∈ dom (𝑔𝑎) ↔ 𝑗 ∈ dom (𝑎)))
187186orbi1d 734 . . . . . . . . . . . . . . . . . 18 ((𝑔𝑎) = (𝑎) → ((𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ (𝑗 ∈ dom (𝑎) ∨ 𝑗 ∈ dom (𝑎))))
188 oridm 534 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ dom (𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ 𝑗 ∈ dom (𝑎))
189187, 188syl6rbb 275 . . . . . . . . . . . . . . . . 17 ((𝑔𝑎) = (𝑎) → (𝑗 ∈ dom (𝑎) ↔ (𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎))))
190 incom 3766 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∩ dom 𝑔) = (dom 𝑔𝑎)
19117, 190eqtri 2631 . . . . . . . . . . . . . . . . . . . 20 dom (𝑔𝑎) = (dom 𝑔𝑎)
192191elin2 3762 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ dom (𝑔𝑎) ↔ (𝑗 ∈ dom 𝑔𝑗𝑎))
193 dmres 5326 . . . . . . . . . . . . . . . . . . . . 21 dom (𝑎) = (𝑎 ∩ dom )
194 incom 3766 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∩ dom ) = (dom 𝑎)
195193, 194eqtri 2631 . . . . . . . . . . . . . . . . . . . 20 dom (𝑎) = (dom 𝑎)
196195elin2 3762 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ dom (𝑎) ↔ (𝑗 ∈ dom 𝑗𝑎))
197192, 196orbi12i 541 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ ((𝑗 ∈ dom 𝑔𝑗𝑎) ∨ (𝑗 ∈ dom 𝑗𝑎)))
198 andir 907 . . . . . . . . . . . . . . . . . 18 (((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑗 ∈ dom 𝑔𝑗𝑎) ∨ (𝑗 ∈ dom 𝑗𝑎)))
199197, 198bitr4i 265 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ dom (𝑔𝑎) ∨ 𝑗 ∈ dom (𝑎)) ↔ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
200189, 199syl6bb 274 . . . . . . . . . . . . . . . 16 ((𝑔𝑎) = (𝑎) → (𝑗 ∈ dom (𝑎) ↔ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
201200pm5.32i 666 . . . . . . . . . . . . . . 15 (((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎)) ↔ ((𝑔𝑎) = (𝑎) ∧ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
202 3anass 1034 . . . . . . . . . . . . . . 15 (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ((𝑔𝑎) = (𝑎) ∧ ((𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎)))
203201, 202bitr4i 265 . . . . . . . . . . . . . 14 (((𝑔𝑎) = (𝑎) ∧ 𝑗 ∈ dom (𝑎)) ↔ ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
204178, 184, 2033bitr3ri 289 . . . . . . . . . . . . 13 (((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
205204rexbii 3022 . . . . . . . . . . . 12 (∃𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑎𝑀𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
206 rexcom4 3197 . . . . . . . . . . . 12 (∃𝑎𝑀𝑏(((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
207205, 206bitri 262 . . . . . . . . . . 11 (∃𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
208207rexbii 3022 . . . . . . . . . 10 (∃𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑅𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
209 rexcom4 3197 . . . . . . . . . 10 (∃𝑅𝑏𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
210208, 209bitri 262 . . . . . . . . 9 (∃𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
211210rexbii 3022 . . . . . . . 8 (∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑔𝐿𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
212 rexcom4 3197 . . . . . . . 8 (∃𝑔𝐿𝑏𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
213171, 211, 2123bitri 284 . . . . . . 7 (∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎) ↔ ∃𝑏𝑔𝐿𝑅𝑎𝑀 (((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
21411rexab 3335 . . . . . . 7 (∃𝑏 ∈ {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}𝑗 ∈ dom 𝑏 ↔ ∃𝑏(∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑏 ∧ (𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
215167, 213, 2143bitr4ri 291 . . . . . 6 (∃𝑏 ∈ {𝑓 ∣ ∃𝑔𝐿𝑅𝑎𝑀 ((𝑔𝑎) = 𝑓 ∧ (𝑎) = 𝑓)}𝑗 ∈ dom 𝑏 ↔ ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
216161, 162, 2153bitri 284 . . . . 5 (𝑗 𝑏𝑆 dom 𝑏 ↔ ∃𝑎𝑀𝑔𝐿𝑅 ((𝑔𝑎) = (𝑎) ∧ (𝑗 ∈ dom 𝑔𝑗 ∈ dom ) ∧ 𝑗𝑎))
217160, 216syl6ibr 240 . . . 4 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → (𝑗 𝑀𝑗 𝑏𝑆 dom 𝑏))
218217ssrdv 3573 . . 3 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 𝑏𝑆 dom 𝑏)
21928, 218eqssd 3584 . 2 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑏𝑆 dom 𝑏 = 𝑀)
2204, 219syl5eq 2655 1 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → dom 𝑋 = 𝑀)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  {cab 2595  wne 2779  wral 2895  wrex 2896  {crab 2899  cin 3538  wss 3539   cuni 4366   cint 4404   ciun 4449   class class class wbr 4577  dom cdm 5028  cres 5030  Rel wrel 5033  Ord word 5625  Oncon0 5626  suc csuc 5628  Fun wfun 5784   No csur 30843   <s cslt 30844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-ord 5629  df-on 5630  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-1o 7424  df-2o 7425  df-no 30846  df-slt 30847  df-bday 30848
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator