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

Theorem noetainflem4 33528
 Description: Lemma for noeta 33531. If 𝐴 precedes 𝐵, then 𝑊 is greater than 𝐴. (Contributed by Scott Fenton, 9-Aug-2024.)
Hypotheses
Ref Expression
noetainflem.1 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
noetainflem.2 𝑊 = (𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
Assertion
Ref Expression
noetainflem4 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑎𝐴 𝑎 <s 𝑊)
Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝐴,𝑎   𝑎,𝑏,𝑔,𝑥,𝐵   𝑣,𝑏,𝑥,𝑦   𝑇,𝑏,𝑔
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑣,𝑢,𝑔,𝑏)   𝑇(𝑥,𝑦,𝑣,𝑢,𝑎)   𝑊(𝑥,𝑦,𝑣,𝑢,𝑔,𝑎,𝑏)

Proof of Theorem noetainflem4
Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplrl 776 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝐵 No )
2 simplrr 777 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝐵 ∈ V)
3 simpll 766 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐴 No )
43sselda 3892 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝑎 No )
5 noetainflem.1 . . . . . 6 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
65noinfbnd2 33519 . . . . 5 ((𝐵 No 𝐵 ∈ V ∧ 𝑎 No ) → (∀𝑏𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
71, 2, 4, 6syl3anc 1368 . . . 4 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → (∀𝑏𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
8 simplll 774 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐴 No )
9 simprl 770 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎𝐴)
108, 9sseldd 3893 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 No )
11 nodmord 33441 . . . . . . . . . 10 (𝑎 No → Ord dom 𝑎)
12 ordirr 6187 . . . . . . . . . 10 (Ord dom 𝑎 → ¬ dom 𝑎 ∈ dom 𝑎)
1310, 11, 123syl 18 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 ∈ dom 𝑎)
14 bdayval 33436 . . . . . . . . . . . . . . 15 (𝑎 No → ( bday 𝑎) = dom 𝑎)
1510, 14syl 17 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday 𝑎) = dom 𝑎)
16 bdayfo 33465 . . . . . . . . . . . . . . . 16 bday : No onto→On
17 fofn 6578 . . . . . . . . . . . . . . . 16 ( bday : No onto→On → bday Fn No )
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 bday Fn No
19 fnfvima 6987 . . . . . . . . . . . . . . 15 (( bday Fn No 𝐴 No 𝑎𝐴) → ( bday 𝑎) ∈ ( bday 𝐴))
2018, 8, 9, 19mp3an2i 1463 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday 𝑎) ∈ ( bday 𝐴))
2115, 20eqeltrrd 2853 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ ( bday 𝐴))
22 elssuni 4830 . . . . . . . . . . . . 13 (dom 𝑎 ∈ ( bday 𝐴) → dom 𝑎 ( bday 𝐴))
2321, 22syl 17 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ( bday 𝐴))
24 nodmon 33438 . . . . . . . . . . . . 13 (𝑎 No → dom 𝑎 ∈ On)
25 imassrn 5912 . . . . . . . . . . . . . . . 16 ( bday 𝐴) ⊆ ran bday
26 forn 6579 . . . . . . . . . . . . . . . . 17 ( bday : No onto→On → ran bday = On)
2716, 26ax-mp 5 . . . . . . . . . . . . . . . 16 ran bday = On
2825, 27sseqtri 3928 . . . . . . . . . . . . . . 15 ( bday 𝐴) ⊆ On
29 ssorduni 7499 . . . . . . . . . . . . . . 15 (( bday 𝐴) ⊆ On → Ord ( bday 𝐴))
3028, 29ax-mp 5 . . . . . . . . . . . . . 14 Ord ( bday 𝐴)
31 ordsssuc 6255 . . . . . . . . . . . . . 14 ((dom 𝑎 ∈ On ∧ Ord ( bday 𝐴)) → (dom 𝑎 ( bday 𝐴) ↔ dom 𝑎 ∈ suc ( bday 𝐴)))
3230, 31mpan2 690 . . . . . . . . . . . . 13 (dom 𝑎 ∈ On → (dom 𝑎 ( bday 𝐴) ↔ dom 𝑎 ∈ suc ( bday 𝐴)))
3310, 24, 323syl 18 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 ( bday 𝐴) ↔ dom 𝑎 ∈ suc ( bday 𝐴)))
3423, 33mpbid 235 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ suc ( bday 𝐴))
35 elun2 4082 . . . . . . . . . . 11 (dom 𝑎 ∈ suc ( bday 𝐴) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ( bday 𝐴)))
3634, 35syl 17 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ( bday 𝐴)))
37 eleq2 2840 . . . . . . . . . 10 (dom 𝑎 = (dom 𝑇 ∪ suc ( bday 𝐴)) → (dom 𝑎 ∈ dom 𝑎 ↔ dom 𝑎 ∈ (dom 𝑇 ∪ suc ( bday 𝐴))))
3836, 37syl5ibrcom 250 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 = (dom 𝑇 ∪ suc ( bday 𝐴)) → dom 𝑎 ∈ dom 𝑎))
3913, 38mtod 201 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 = (dom 𝑇 ∪ suc ( bday 𝐴)))
40 dmeq 5743 . . . . . . . . 9 (𝑎 = 𝑊 → dom 𝑎 = dom 𝑊)
41 noetainflem.2 . . . . . . . . . . 11 𝑊 = (𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
4241dmeqi 5744 . . . . . . . . . 10 dom 𝑊 = dom (𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
43 dmun 5750 . . . . . . . . . 10 dom (𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
44 2oex 8122 . . . . . . . . . . . . . 14 2o ∈ V
4544snnz 4669 . . . . . . . . . . . . 13 {2o} ≠ ∅
46 dmxp 5770 . . . . . . . . . . . . 13 ({2o} ≠ ∅ → dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) = (suc ( bday 𝐴) ∖ dom 𝑇))
4745, 46ax-mp 5 . . . . . . . . . . . 12 dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) = (suc ( bday 𝐴) ∖ dom 𝑇)
4847uneq2i 4065 . . . . . . . . . . 11 (dom 𝑇 ∪ dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ (suc ( bday 𝐴) ∖ dom 𝑇))
49 undif2 4373 . . . . . . . . . . 11 (dom 𝑇 ∪ (suc ( bday 𝐴) ∖ dom 𝑇)) = (dom 𝑇 ∪ suc ( bday 𝐴))
5048, 49eqtri 2781 . . . . . . . . . 10 (dom 𝑇 ∪ dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ suc ( bday 𝐴))
5142, 43, 503eqtri 2785 . . . . . . . . 9 dom 𝑊 = (dom 𝑇 ∪ suc ( bday 𝐴))
5240, 51eqtrdi 2809 . . . . . . . 8 (𝑎 = 𝑊 → dom 𝑎 = (dom 𝑇 ∪ suc ( bday 𝐴)))
5339, 52nsyl 142 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ 𝑎 = 𝑊)
5453neqned 2958 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎𝑊)
55 simpr 488 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇)
5610adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝑎 No )
5756adantr 484 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → 𝑎 No )
58 simp-4r 783 . . . . . . . . . . . . . . . . . 18 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝐴 ∈ V)
59 simplrl 776 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 No )
6059adantr 484 . . . . . . . . . . . . . . . . . 18 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝐵 No )
61 simplrr 777 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ∈ V)
6261adantr 484 . . . . . . . . . . . . . . . . . 18 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝐵 ∈ V)
635, 41noetainflem1 33525 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ 𝐵 No 𝐵 ∈ V) → 𝑊 No )
6458, 60, 62, 63syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝑊 No )
6564adantr 484 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → 𝑊 No )
66 simplr 768 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → 𝑎𝑊)
67 nosepne 33468 . . . . . . . . . . . . . . . 16 ((𝑎 No 𝑊 No 𝑎𝑊) → (𝑎 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) ≠ (𝑊 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
6857, 65, 66, 67syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑎 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) ≠ (𝑊 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
6955fvresd 6678 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = (𝑊 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
70 simp-4r 783 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝐵 No 𝐵 ∈ V))
715, 41noetainflem2 33526 . . . . . . . . . . . . . . . . . 18 ((𝐵 No 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
7270, 71syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
7372fveq1d 6660 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = (𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
7469, 73eqtr3d 2795 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑊 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = (𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
7568, 74neeqtrd 3020 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑎 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) ≠ (𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
7675necomd 3006 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) ≠ (𝑎 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
77 fveq2 6658 . . . . . . . . . . . . . . 15 (𝑞 = {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} → (𝑇𝑞) = (𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
78 fveq2 6658 . . . . . . . . . . . . . . 15 (𝑞 = {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} → (𝑎𝑞) = (𝑎 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
7977, 78neeq12d 3012 . . . . . . . . . . . . . 14 (𝑞 = {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} → ((𝑇𝑞) ≠ (𝑎𝑞) ↔ (𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) ≠ (𝑎 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)})))
8079rspcev 3541 . . . . . . . . . . . . 13 (( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇 ∧ (𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) ≠ (𝑎 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)})) → ∃𝑞 ∈ dom 𝑇(𝑇𝑞) ≠ (𝑎𝑞))
8155, 76, 80syl2anc 587 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ∃𝑞 ∈ dom 𝑇(𝑇𝑞) ≠ (𝑎𝑞))
82 df-ne 2952 . . . . . . . . . . . . . . 15 ((𝑇𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ (𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
83 fvres 6677 . . . . . . . . . . . . . . . 16 (𝑞 ∈ dom 𝑇 → ((𝑎 ↾ dom 𝑇)‘𝑞) = (𝑎𝑞))
8483neeq2d 3011 . . . . . . . . . . . . . . 15 (𝑞 ∈ dom 𝑇 → ((𝑇𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇𝑞) ≠ (𝑎𝑞)))
8582, 84bitr3id 288 . . . . . . . . . . . . . 14 (𝑞 ∈ dom 𝑇 → (¬ (𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇𝑞) ≠ (𝑎𝑞)))
8685rexbiia 3174 . . . . . . . . . . . . 13 (∃𝑞 ∈ dom 𝑇 ¬ (𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ∃𝑞 ∈ dom 𝑇(𝑇𝑞) ≠ (𝑎𝑞))
87 rexnal 3165 . . . . . . . . . . . . 13 (∃𝑞 ∈ dom 𝑇 ¬ (𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
8886, 87bitr3i 280 . . . . . . . . . . . 12 (∃𝑞 ∈ dom 𝑇(𝑇𝑞) ≠ (𝑎𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
8981, 88sylib 221 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
9089olcd 871 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
915noinfno 33506 . . . . . . . . . . . . . . . 16 ((𝐵 No 𝐵 ∈ V) → 𝑇 No )
9291ad3antlr 730 . . . . . . . . . . . . . . 15 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝑇 No )
9392adantr 484 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → 𝑇 No )
94 nofun 33437 . . . . . . . . . . . . . 14 (𝑇 No → Fun 𝑇)
9593, 94syl 17 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → Fun 𝑇)
96 nofun 33437 . . . . . . . . . . . . . 14 (𝑎 No → Fun 𝑎)
97 funres 6377 . . . . . . . . . . . . . 14 (Fun 𝑎 → Fun (𝑎 ↾ dom 𝑇))
9857, 96, 973syl 18 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → Fun (𝑎 ↾ dom 𝑇))
99 eqfunfv 6798 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ Fun (𝑎 ↾ dom 𝑇)) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
10095, 98, 99syl2anc 587 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
101 ianor 979 . . . . . . . . . . . . 13 (¬ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
102101con1bii 360 . . . . . . . . . . . 12 (¬ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
103100, 102bitr4di 292 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ ¬ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
104103con2bid 358 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ((¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ ¬ 𝑇 = (𝑎 ↾ dom 𝑇)))
10590, 104mpbid 235 . . . . . . . . 9 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ¬ 𝑇 = (𝑎 ↾ dom 𝑇))
106105pm2.21d 121 . . . . . . . 8 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊))
10772breq2d 5044 . . . . . . . . 9 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) ↔ (𝑎 ↾ dom 𝑇) <s 𝑇))
108 nodmon 33438 . . . . . . . . . . . 12 (𝑇 No → dom 𝑇 ∈ On)
10992, 108syl 17 . . . . . . . . . . 11 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → dom 𝑇 ∈ On)
110109adantr 484 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → dom 𝑇 ∈ On)
111 sltres 33450 . . . . . . . . . 10 ((𝑎 No 𝑊 No ∧ dom 𝑇 ∈ On) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
11257, 65, 110, 111syl3anc 1368 . . . . . . . . 9 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
113107, 112sylbird 263 . . . . . . . 8 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s 𝑇𝑎 <s 𝑊))
114 simplrr 777 . . . . . . . . . 10 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
115114adantr 484 . . . . . . . . 9 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
116 noreson 33448 . . . . . . . . . . . . 13 ((𝑎 No ∧ dom 𝑇 ∈ On) → (𝑎 ↾ dom 𝑇) ∈ No )
11756, 109, 116syl2anc 587 . . . . . . . . . . . 12 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → (𝑎 ↾ dom 𝑇) ∈ No )
118117adantr 484 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑎 ↾ dom 𝑇) ∈ No )
119 sltso 33464 . . . . . . . . . . . 12 <s Or No
120 sotric 5470 . . . . . . . . . . . 12 (( <s Or No ∧ (𝑇 No ∧ (𝑎 ↾ dom 𝑇) ∈ No )) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
121119, 120mpan 689 . . . . . . . . . . 11 ((𝑇 No ∧ (𝑎 ↾ dom 𝑇) ∈ No ) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
12293, 118, 121syl2anc 587 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
123122con2bid 358 . . . . . . . . 9 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → ((𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇) ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
124115, 123mpbird 260 . . . . . . . 8 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇))
125106, 113, 124mpjaod 857 . . . . . . 7 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇) → 𝑎 <s 𝑊)
12664adantr 484 . . . . . . . 8 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑊 No )
12756adantr 484 . . . . . . . 8 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑎 No )
128 simplr 768 . . . . . . . . 9 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑎𝑊)
129128necomd 3006 . . . . . . . 8 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑊𝑎)
13041fveq1i 6659 . . . . . . . . 9 (𝑊 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = ((𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)})
13192adantr 484 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑇 No )
132131, 94syl 17 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → Fun 𝑇)
133132funfnd 6366 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑇 Fn dom 𝑇)
134 fnconstg 6552 . . . . . . . . . . . . 13 (2o ∈ V → ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ( bday 𝐴) ∖ dom 𝑇))
13544, 134ax-mp 5 . . . . . . . . . . . 12 ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ( bday 𝐴) ∖ dom 𝑇)
136135a1i 11 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ( bday 𝐴) ∖ dom 𝑇))
137 disjdif 4368 . . . . . . . . . . . 12 (dom 𝑇 ∩ (suc ( bday 𝐴) ∖ dom 𝑇)) = ∅
138137a1i 11 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → (dom 𝑇 ∩ (suc ( bday 𝐴) ∖ dom 𝑇)) = ∅)
139 nosepssdm 33474 . . . . . . . . . . . . . 14 ((𝑎 No 𝑊 No 𝑎𝑊) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ⊆ dom 𝑎)
140127, 126, 128, 139syl3anc 1368 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ⊆ dom 𝑎)
141127, 14syl 17 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → ( bday 𝑎) = dom 𝑎)
142 simp-5l 784 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝐴 No )
143 simplrl 776 . . . . . . . . . . . . . . . . . 18 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝑎𝐴)
144143adantr 484 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑎𝐴)
14518, 142, 144, 19mp3an2i 1463 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → ( bday 𝑎) ∈ ( bday 𝐴))
146 elssuni 4830 . . . . . . . . . . . . . . . 16 (( bday 𝑎) ∈ ( bday 𝐴) → ( bday 𝑎) ⊆ ( bday 𝐴))
147145, 146syl 17 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → ( bday 𝑎) ⊆ ( bday 𝐴))
148141, 147eqsstrrd 3931 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → dom 𝑎 ( bday 𝐴))
149127, 24, 323syl 18 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → (dom 𝑎 ( bday 𝐴) ↔ dom 𝑎 ∈ suc ( bday 𝐴)))
150148, 149mpbid 235 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → dom 𝑎 ∈ suc ( bday 𝐴))
151 simpr 488 . . . . . . . . . . . . . . . 16 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝑎𝑊)
152 nosepon 33453 . . . . . . . . . . . . . . . 16 ((𝑎 No 𝑊 No 𝑎𝑊) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ On)
15356, 64, 151, 152syl3anc 1368 . . . . . . . . . . . . . . 15 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ On)
154153adantr 484 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ On)
155 eloni 6179 . . . . . . . . . . . . . 14 ( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ On → Ord {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)})
156 ordsuc 7528 . . . . . . . . . . . . . . . 16 (Ord ( bday 𝐴) ↔ Ord suc ( bday 𝐴))
15730, 156mpbi 233 . . . . . . . . . . . . . . 15 Ord suc ( bday 𝐴)
158 ordtr2 6213 . . . . . . . . . . . . . . 15 ((Ord {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∧ Ord suc ( bday 𝐴)) → (( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ( bday 𝐴)) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ suc ( bday 𝐴)))
159157, 158mpan2 690 . . . . . . . . . . . . . 14 (Ord {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} → (( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ( bday 𝐴)) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ suc ( bday 𝐴)))
160154, 155, 1593syl 18 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → (( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ( bday 𝐴)) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ suc ( bday 𝐴)))
161140, 150, 160mp2and 698 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ suc ( bday 𝐴))
162 ontri1 6203 . . . . . . . . . . . . . 14 ((dom 𝑇 ∈ On ∧ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ On) → (dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇))
163109, 153, 162syl2anc 587 . . . . . . . . . . . . 13 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → (dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇))
164163biimpa 480 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → ¬ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇)
165161, 164eldifd 3869 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ (suc ( bday 𝐴) ∖ dom 𝑇))
166133, 136, 138, 165fvun2d 6746 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → ((𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
16744fvconst2 6957 . . . . . . . . . . 11 ( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ (suc ( bday 𝐴) ∖ dom 𝑇) → (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = 2o)
168165, 167syl 17 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = 2o)
169166, 168eqtrd 2793 . . . . . . . . 9 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → ((𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))‘ {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = 2o)
170130, 169syl5eq 2805 . . . . . . . 8 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → (𝑊 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = 2o)
171 nosep2o 33470 . . . . . . . 8 (((𝑊 No 𝑎 No 𝑊𝑎) ∧ (𝑊 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) = 2o) → 𝑎 <s 𝑊)
172126, 127, 129, 170, 171syl31anc 1370 . . . . . . 7 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) ∧ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}) → 𝑎 <s 𝑊)
173153, 155syl 17 . . . . . . . 8 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → Ord {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)})
174 nodmord 33441 . . . . . . . . 9 (𝑇 No → Ord dom 𝑇)
17592, 174syl 17 . . . . . . . 8 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → Ord dom 𝑇)
176 ordtri2or 6264 . . . . . . . 8 ((Ord {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∧ Ord dom 𝑇) → ( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
177173, 175, 176syl2anc 587 . . . . . . 7 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → ( {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 {𝑝 ∈ On ∣ (𝑎𝑝) ≠ (𝑊𝑝)}))
178125, 172, 177mpjaodan 956 . . . . . 6 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎𝑊) → 𝑎 <s 𝑊)
17954, 178mpdan 686 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑎𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 <s 𝑊)
180179expr 460 . . . 4 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → (¬ 𝑇 <s (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊))
1817, 180sylbid 243 . . 3 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → (∀𝑏𝐵 𝑎 <s 𝑏𝑎 <s 𝑊))
182181ralimdva 3108 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏 → ∀𝑎𝐴 𝑎 <s 𝑊))
1831823impia 1114 1 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑎𝐴 𝑎 <s 𝑊)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2735   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  {crab 3074  Vcvv 3409   ∖ cdif 3855   ∪ cun 3856   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  ifcif 4420  {csn 4522  ⟨cop 4528  ∪ cuni 4798  ∩ cint 4838   class class class wbr 5032   ↦ cmpt 5112   Or wor 5442   × cxp 5522  dom cdm 5524  ran crn 5525   ↾ cres 5526   “ cima 5527  Ord word 6168  Oncon0 6169  suc csuc 6171  ℩cio 6292  Fun wfun 6329   Fn wfn 6330  –onto→wfo 6333  ‘cfv 6335  ℩crio 7107  1oc1o 8105  2oc2o 8106   No csur 33428
 Copyright terms: Public domain W3C validator