noinfbnd2lem1 - Metamath Proof Explorer

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

Theorem noinfbnd2lem1 27860

Description: Bounding law from below when a set of surreals has a minimum. (Contributed by Scott Fenton, 9-Aug-2024.)

**Assertion**
Ref	Expression
noinfbnd2lem1	⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))

Distinct variable groups: 𝐵,𝑏 𝑈,𝑏 𝑍,𝑏 Allowed substitution hints: 𝐵(𝑦) 𝑈(𝑦) 𝑉(𝑦,𝑏) 𝑍(𝑦)

Proof of Theorem noinfbnd2lem1 Dummy variables 𝑞 𝑝 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5117	. . 3 ⊢ (𝑏 = 𝑈 → (𝑍 <s 𝑏 ↔ 𝑍 <s 𝑈))
2		simp3 1154	. . 3 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
3		simp1l 1214	. . 3 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → 𝑈 ∈ 𝐵)
4	1, 2, 3	rspcdva 3591	. 2 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → 𝑍 <s 𝑈)
5		simpl21 1268	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝐵 ⊆ No )
6		simpl1l 1241	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ∈ 𝐵)
7	5, 6	sseldd 3946	. . . . . . . . . 10 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ∈ No )
8		nodmon 27780	. . . . . . . . . 10 ⊢ (𝑈 ∈ No → dom 𝑈 ∈ On)
9	7, 8	syl 18	. . . . . . . . 9 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → dom 𝑈 ∈ On)
10		onelon 6386	. . . . . . . . 9 ⊢ ((dom 𝑈 ∈ On ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
11	9, 10	sylan 591	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
12		simpr 489	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})
13		simplr 780	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈)
14	9	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
15	14	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → dom 𝑈 ∈ On)
16		ontr1 6409	. . . . . . . . . . . . 13 ⊢ (dom 𝑈 ∈ On → ((𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
17	15, 16	syl 18	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
18	12, 13, 17	mp2and 711	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ dom 𝑈)
19	18	fvresd 6902	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞))
20		onelon 6386	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On)
21	11, 20	sylan 591	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On)
22		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑈‘𝑥) = (𝑈‘𝑞))
23		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑍‘𝑥) = (𝑍‘𝑞))
24	22, 23	neeq12d 3025	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑈‘𝑞) ≠ (𝑍‘𝑞)))
25	24	onnminsb 7798	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ On → (𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)))
26	21, 12, 25	sylc 66	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
27		df-ne 2965	. . . . . . . . . . . 12 ⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) = (𝑍‘𝑞))
28	27	con2bii 360	. . . . . . . . . . 11 ⊢ ((𝑈‘𝑞) = (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
29	26, 28	sylibr 237	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → (𝑈‘𝑞) = (𝑍‘𝑞))
30	19, 29	eqtr4d 2807	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
31	30	ralrimiva 3163	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
32		simpr 489	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈)
33	32	fvresd 6902	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
34		simplr 780	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑍 <s 𝑈)
35		simpl23 1270	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 ∈ No )
36	7	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 ∈ No )
37		ltsval2 27786	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ No ∧ 𝑈 ∈ No ) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})))
38	35, 36, 37	syl2an2r 697	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})))
39	34, 38	mpbid 235	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))
40		necom 3017	. . . . . . . . . . . . 13 ⊢ ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑍‘𝑥) ≠ (𝑈‘𝑥))
41	40	rabbii 3428	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}
42	41	inteqi 4920	. . . . . . . . . . 11 ⊢ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}
43	42	fveq2i 6885	. . . . . . . . . 10 ⊢ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})
44	42	fveq2i 6885	. . . . . . . . . 10 ⊢ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})
45	39, 43, 44	3brtr4g 5149	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
46	33, 45	eqbrtrd 5137	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
47		raleq 3326	. . . . . . . . . 10 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ↔ ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))
48		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
49		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (𝑈‘𝑝) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
50	48, 49	breq12d 5126	. . . . . . . . . 10 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝) ↔ ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})))
51	47, 50	anbi12d 643	. . . . . . . . 9 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝)) ↔ (∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))))
52	51	rspcev 3590	. . . . . . . 8 ⊢ ((∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ (∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝)))
53	11, 31, 46, 52	syl12anc 849	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝)))
54		noreson 27790	. . . . . . . . 9 ⊢ ((𝑍 ∈ No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
55	35, 9, 54	syl2anc 595	. . . . . . . 8 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
56		ltsval 27777	. . . . . . . 8 ⊢ (((𝑍 ↾ dom 𝑈) ∈ No ∧ 𝑈 ∈ No ) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝))))
57	55, 36, 56	syl2an2r 697	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝))))
58	53, 57	mpbird 260	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) <s 𝑈)
59		sssucid 6444	. . . . . . 7 ⊢ dom 𝑈 ⊆ suc dom 𝑈
60		resabs1 6006	. . . . . . 7 ⊢ (dom 𝑈 ⊆ suc dom 𝑈 → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
61	59, 60	mp1i 14	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
62		resundir 5994	. . . . . . 7 ⊢ ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈))
63		nofun 27779	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ No → Fun 𝑈)
64	7, 63	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑈)
65		funrel 6554	. . . . . . . . . . . 12 ⊢ (Fun 𝑈 → Rel 𝑈)
66	64, 65	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Rel 𝑈)
67	66	adantr 485	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → Rel 𝑈)
68		resdm 6026	. . . . . . . . . 10 ⊢ (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
69	67, 68	syl 18	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
70		nodmord 27783	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ No → Ord dom 𝑈)
71	7, 70	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Ord dom 𝑈)
72	71	adantr 485	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → Ord dom 𝑈)
73		ordirr 6379	. . . . . . . . . . 11 ⊢ (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
74	72, 73	syl 18	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
75		1oex 8463	. . . . . . . . . . 11 ⊢ 1_o ∈ V
76	75	snres0 6300	. . . . . . . . . 10 ⊢ (({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
77	74, 76	sylibr 237	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈) = ∅)
78	69, 77	uneq12d 4131	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈)) = (𝑈 ∪ ∅))
79		un0 4358	. . . . . . . 8 ⊢ (𝑈 ∪ ∅) = 𝑈
80	78, 79	eqtrdi 2820	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈)) = 𝑈)
81	62, 80	eqtrid 2816	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈) = 𝑈)
82	58, 61, 81	3brtr4d 5147	. . . . 5 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈))
83		onsucb 7813	. . . . . . . . 9 ⊢ (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
84	9, 83	sylib 221	. . . . . . . 8 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → suc dom 𝑈 ∈ On)
85		noreson 27790	. . . . . . . 8 ⊢ ((𝑍 ∈ No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
86	35, 84, 85	syl2anc 595	. . . . . . 7 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
87	86	adantr 485	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
88	75	prid1 4733	. . . . . . . . 9 ⊢ 1_o ∈ {1_o, 2_o}
89	88	noextend 27796	. . . . . . . 8 ⊢ (𝑈 ∈ No → (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No )
90	7, 89	syl 18	. . . . . . 7 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No )
91	90	adantr 485	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No )
92		ltsres 27792	. . . . . 6 ⊢ (((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No ∧ dom 𝑈 ∈ On) → (((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩})))
93	87, 91, 14, 92	syl3anc 1396	. . . . 5 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩})))
94	82, 93	mpd 16	. . . 4 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
95		ltsso 27806	. . . . . 6 ⊢ <s Or No
96		soasym 5603	. . . . . 6 ⊢ (( <s Or No ∧ ((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No )) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
97	95, 96	mpan 702	. . . . 5 ⊢ (((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No ) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
98	86, 91, 97	syl2an2r 697	. . . 4 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
99	94, 98	mpd 16	. . 3 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))
100		sonr 5594	. . . . . 6 ⊢ (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
101	95, 90, 100	sylancr 598	. . . . 5 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
102	101	adantr 485	. . . 4 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
103		df-suc 6367	. . . . . . . 8 ⊢ suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
104	103	reseq2i 5976	. . . . . . 7 ⊢ (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
105		resundi 5993	. . . . . . 7 ⊢ (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
106	104, 105	eqtri 2792	. . . . . 6 ⊢ (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
107		dmres 6012	. . . . . . . . 9 ⊢ dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
108	42	eqeq1i 2774	. . . . . . . . . . . 12 ⊢ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 ↔ ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} = dom 𝑈)
109	108	bilani 509	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} = dom 𝑈)
110	35	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ∈ No )
111	7	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 ∈ No )
112		simp23 1225	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → 𝑍 ∈ No )
113		sonr 5594	. . . . . . . . . . . . . . . . . 18 ⊢ (( <s Or No ∧ 𝑍 ∈ No ) → ¬ 𝑍 <s 𝑍)
114	95, 112, 113	sylancr 598	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑍 <s 𝑍)
115		breq2 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 = 𝑍 → (𝑍 <s 𝑈 ↔ 𝑍 <s 𝑍))
116	115	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 = 𝑍 → (¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍))
117	114, 116	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → (𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈))
118	117	necon2ad 2979	. . . . . . . . . . . . . . 15 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → (𝑍 <s 𝑈 → 𝑈 ≠ 𝑍))
119	118	imp 411	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ≠ 𝑍)
120	119	necomd 3019	. . . . . . . . . . . . 13 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 ≠ 𝑈)
121	120	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ≠ 𝑈)
122		nosepssdm 27816	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ No ∧ 𝑈 ∈ No ∧ 𝑍 ≠ 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍)
123	110, 111, 121, 122	syl3anc 1396	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍)
124	109, 123	eqsstrrd 3980	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
125		dfss2 3931	. . . . . . . . . 10 ⊢ (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
126	124, 125	sylib 221	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
127	107, 126	eqtrid 2816	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
128	127	eleq2d 2855	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
129		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
130	129	fvresd 6902	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞))
131	111, 8	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ On)
132		onelon 6386	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
133	131, 132	sylan 591	. . . . . . . . . . . . . 14 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
134		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)
135	134	eleq2d 2855	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ↔ 𝑞 ∈ dom 𝑈))
136	135	biimpar 482	. . . . . . . . . . . . . 14 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})
137	133, 136, 25	sylc 66	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
138		nesym 3020	. . . . . . . . . . . . . 14 ⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑍‘𝑞) = (𝑈‘𝑞))
139	138	con2bii 360	. . . . . . . . . . . . 13 ⊢ ((𝑍‘𝑞) = (𝑈‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
140	137, 139	sylibr 237	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍‘𝑞) = (𝑈‘𝑞))
141	130, 140	eqtrd 2804	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
142	141	ex 417	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))
143	128, 142	sylbid 243	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))
144	143	ralrimiv 3162	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
145		nofun 27779	. . . . . . . . . . 11 ⊢ (𝑍 ∈ No → Fun 𝑍)
146	110, 145	syl 18	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑍)
147	146	funresd 6580	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈))
148	64	adantr 485	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑈)
149		eqfunfv 7032	. . . . . . . . 9 ⊢ ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))))
150	147, 148, 149	syl2anc 595	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))))
151	127, 144, 150	mpbir2and 725	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈)
152	35, 145	syl 18	. . . . . . . . . 10 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑍)
153	152	funfnd 6568	. . . . . . . . 9 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 Fn dom 𝑍)
154		ndmfv 6914	. . . . . . . . . . . . . . . 16 ⊢ (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
155		2on0 8468	. . . . . . . . . . . . . . . . . . 19 ⊢ 2_o ≠ ∅
156	155	necomi 3018	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ≠ 2_o
157		neeq1 3026	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈‘dom 𝑈) = ∅ → ((𝑈‘dom 𝑈) ≠ 2_o ↔ ∅ ≠ 2_o))
158	156, 157	mpbiri 261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘dom 𝑈) = ∅ → (𝑈‘dom 𝑈) ≠ 2_o)
159	158	neneqd 2969	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈‘dom 𝑈) = ∅ → ¬ (𝑈‘dom 𝑈) = 2_o)
160	154, 159	syl 18	. . . . . . . . . . . . . . 15 ⊢ (¬ dom 𝑈 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑈) = 2_o)
161	111, 70, 73, 160	4syl 20	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 2_o)
162	161	intnand 493	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2_o))
163		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 <s 𝑈)
164	35, 7, 37	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})))
165	163, 164	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))
166	165	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))
167	109	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) = (𝑍‘dom 𝑈))
168	109	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) = (𝑈‘dom 𝑈))
169	166, 167, 168	3brtr3d 5146	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘dom 𝑈))
170		fvex 6895	. . . . . . . . . . . . . . 15 ⊢ (𝑍‘dom 𝑈) ∈ V
171		fvex 6895	. . . . . . . . . . . . . . 15 ⊢ (𝑈‘dom 𝑈) ∈ V
172	170, 171	brtp 5508	. . . . . . . . . . . . . 14 ⊢ ((𝑍‘dom 𝑈){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘dom 𝑈) ↔ (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2_o)))
173	169, 172	sylib 221	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2_o)))
174		3orel3 1514	. . . . . . . . . . . . 13 ⊢ (¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2_o) → ((((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2_o)) → (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o))))
175	162, 173, 174	sylc 66	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o)))
176		andi 1023	. . . . . . . . . . . 12 ⊢ (((𝑍‘dom 𝑈) = 1_o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2_o)) ↔ (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o)))
177	175, 176	sylibr 237	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍‘dom 𝑈) = 1_o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2_o)))
178	177	simpld 499	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 1_o)
179		ndmfv 6914	. . . . . . . . . . . 12 ⊢ (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
180		1n0 8472	. . . . . . . . . . . . . . 15 ⊢ 1_o ≠ ∅
181	180	necomi 3018	. . . . . . . . . . . . . 14 ⊢ ∅ ≠ 1_o
182		neeq1 3026	. . . . . . . . . . . . . 14 ⊢ ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 1_o ↔ ∅ ≠ 1_o))
183	181, 182	mpbiri 261	. . . . . . . . . . . . 13 ⊢ ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 1_o)
184	183	neneqd 2969	. . . . . . . . . . . 12 ⊢ ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 1_o)
185	179, 184	syl 18	. . . . . . . . . . 11 ⊢ (¬ dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 1_o)
186	185	con4i 115	. . . . . . . . . 10 ⊢ ((𝑍‘dom 𝑈) = 1_o → dom 𝑈 ∈ dom 𝑍)
187	178, 186	syl 18	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍)
188		fnressn 7156	. . . . . . . . 9 ⊢ ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
189	153, 187, 188	syl2an2r 697	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
190	178	opeq2d 4849	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 1_o⟩)
191	190	sneqd 4606	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 1_o⟩})
192	189, 191	eqtrd 2804	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 1_o⟩})
193	151, 192	uneq12d 4131	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
194	106, 193	eqtrid 2816	. . . . 5 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
195	194	breq2d 5125	. . . 4 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈) ↔ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩})))
196	102, 195	mtbird 328	. . 3 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))
197		nosepssdm 27816	. . . . 5 ⊢ ((𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈)
198	7, 35, 119, 197	syl3anc 1396	. . . 4 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈)
199		nosepon 27795	. . . . . 6 ⊢ ((𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
200	7, 35, 119, 199	syl3anc 1396	. . . . 5 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
201		onsseleq 6403	. . . . 5 ⊢ ((∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)))
202	200, 9, 201	syl2anc 595	. . . 4 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)))
203	198, 202	mpbid 235	. . 3 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))
204	99, 196, 203	mpjaodan 973	. 2 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))
205	4, 204	mpdan 699	1 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∨ w3o 1100 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 {crab 3423 ∪ cun 3911 ∩ cin 3912 ⊆ wss 3913 ∅c0 4294 {csn 4594 {ctp 4598 ⟨cop 4600 ∩ cint 4916 class class class wbr 5113 Or wor 5569 dom cdm 5662 ↾ cres 5664 Rel wrel 5667 Ord word 6360 Oncon0 6361 suc csuc 6363 Fun wfun 6531 Fn wfn 6532 ‘cfv 6537 1_oc1o 8446 2_oc2o 8447 No csur 27770 <s clts 27771

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-ord 6364 df-on 6365 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-1o 8453 df-2o 8454 df-no 27773 df-lts 27774

This theorem is referenced by: noinfbnd2 27861

W3C validator