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 27712

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 5076	. . 3 ⊢ (𝑏 = 𝑈 → (𝑍 <s 𝑏 ↔ 𝑍 <s 𝑈))
2		simp3 1144	. . 3 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
3		simp1l 1204	. . 3 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → 𝑈 ∈ 𝐵)
4	1, 2, 3	rspcdva 3561	. 2 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → 𝑍 <s 𝑈)
5		simpl21 1258	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝐵 ⊆ No )
6		simpl1l 1231	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ∈ 𝐵)
7	5, 6	sseldd 3916	. . . . . . . . . 10 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ∈ No )
8		nodmon 27632	. . . . . . . . . 10 ⊢ (𝑈 ∈ No → dom 𝑈 ∈ On)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → dom 𝑈 ∈ On)
10		onelon 6335	. . . . . . . . 9 ⊢ ((dom 𝑈 ∈ On ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
11	9, 10	sylan 586	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
12		simpr 485	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})
13		simplr 774	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈)
14	9	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
15	14	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → dom 𝑈 ∈ On)
16		ontr1 6357	. . . . . . . . . . . . 13 ⊢ (dom 𝑈 ∈ On → ((𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
17	15, 16	syl 17	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
18	12, 13, 17	mp2and 705	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ dom 𝑈)
19	18	fvresd 6847	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞))
20		onelon 6335	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On)
21	11, 20	sylan 586	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On)
22		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑈‘𝑥) = (𝑈‘𝑞))
23		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑍‘𝑥) = (𝑍‘𝑞))
24	22, 23	neeq12d 2995	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑈‘𝑞) ≠ (𝑍‘𝑞)))
25	24	onnminsb 7742	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ On → (𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)))
26	21, 12, 25	sylc 65	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
27		df-ne 2935	. . . . . . . . . . . 12 ⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) = (𝑍‘𝑞))
28	27	con2bii 358	. . . . . . . . . . 11 ⊢ ((𝑈‘𝑞) = (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
29	26, 28	sylibr 235	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → (𝑈‘𝑞) = (𝑍‘𝑞))
30	19, 29	eqtr4d 2777	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
31	30	ralrimiva 3131	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
32		simpr 485	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈)
33	32	fvresd 6847	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
34		simplr 774	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑍 <s 𝑈)
35		simpl23 1260	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 ∈ No )
36	7	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 ∈ No )
37		ltsval2 27638	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ No ∧ 𝑈 ∈ No ) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})))
38	35, 36, 37	syl2an2r 691	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})))
39	34, 38	mpbid 233	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))
40		necom 2987	. . . . . . . . . . . . 13 ⊢ ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑍‘𝑥) ≠ (𝑈‘𝑥))
41	40	rabbii 3396	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}
42	41	inteqi 4881	. . . . . . . . . . 11 ⊢ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}
43	42	fveq2i 6830	. . . . . . . . . 10 ⊢ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})
44	42	fveq2i 6830	. . . . . . . . . 10 ⊢ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})
45	39, 43, 44	3brtr4g 5106	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
46	33, 45	eqbrtrd 5094	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
47		raleq 3294	. . . . . . . . . 10 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ↔ ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))
48		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
49		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑝 = ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (𝑈‘𝑝) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))
50	48, 49	breq12d 5085	. . . . . . . . . 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 638	. . . . . . . . 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 3560	. . . . . . . 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 842	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝)))
54		noreson 27642	. . . . . . . . 9 ⊢ ((𝑍 ∈ No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
55	35, 9, 54	syl2anc 590	. . . . . . . 8 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
56		ltsval 27629	. . . . . . . 8 ⊢ (((𝑍 ↾ dom 𝑈) ∈ No ∧ 𝑈 ∈ No ) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘𝑝))))
57	55, 36, 56	syl2an2r 691	. . . . . . 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 258	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) <s 𝑈)
59		sssucid 6392	. . . . . . 7 ⊢ dom 𝑈 ⊆ suc dom 𝑈
60		resabs1 5958	. . . . . . 7 ⊢ (dom 𝑈 ⊆ suc dom 𝑈 → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
61	59, 60	mp1i 13	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
62		resundir 5946	. . . . . . 7 ⊢ ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈))
63		nofun 27631	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ No → Fun 𝑈)
64	7, 63	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑈)
65		funrel 6502	. . . . . . . . . . . 12 ⊢ (Fun 𝑈 → Rel 𝑈)
66	64, 65	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Rel 𝑈)
67	66	adantr 481	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → Rel 𝑈)
68		resdm 5978	. . . . . . . . . 10 ⊢ (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
69	67, 68	syl 17	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
70		nodmord 27635	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ No → Ord dom 𝑈)
71	7, 70	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Ord dom 𝑈)
72	71	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → Ord dom 𝑈)
73		ordirr 6328	. . . . . . . . . . 11 ⊢ (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
74	72, 73	syl 17	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
75		1oex 8405	. . . . . . . . . . 11 ⊢ 1_o ∈ V
76	75	snres0 6249	. . . . . . . . . 10 ⊢ (({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
77	74, 76	sylibr 235	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈) = ∅)
78	69, 77	uneq12d 4099	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈)) = (𝑈 ∪ ∅))
79		un0 4322	. . . . . . . 8 ⊢ (𝑈 ∪ ∅) = 𝑈
80	78, 79	eqtrdi 2790	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1_o⟩} ↾ dom 𝑈)) = 𝑈)
81	62, 80	eqtrid 2786	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈) = 𝑈)
82	58, 61, 81	3brtr4d 5104	. . . . 5 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ↾ dom 𝑈))
83		onsucb 7757	. . . . . . . . 9 ⊢ (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
84	9, 83	sylib 219	. . . . . . . 8 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → suc dom 𝑈 ∈ On)
85		noreson 27642	. . . . . . . 8 ⊢ ((𝑍 ∈ No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
86	35, 84, 85	syl2anc 590	. . . . . . 7 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
87	86	adantr 481	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
88	75	prid1 4694	. . . . . . . . 9 ⊢ 1_o ∈ {1_o, 2_o}
89	88	noextend 27648	. . . . . . . 8 ⊢ (𝑈 ∈ No → (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No )
90	7, 89	syl 17	. . . . . . 7 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No )
91	90	adantr 481	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No )
92		ltsres 27644	. . . . . 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 1379	. . . . 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 15	. . . 4 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
95		ltsso 27658	. . . . . 6 ⊢ <s Or No
96		soasym 5559	. . . . . 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 696	. . . . 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 691	. . . 4 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
99	94, 98	mpd 15	. . 3 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))
100		sonr 5550	. . . . . 6 ⊢ (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
101	95, 90, 100	sylancr 593	. . . . 5 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
102	101	adantr 481	. . . 4 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
103		df-suc 6316	. . . . . . . 8 ⊢ suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
104	103	reseq2i 5928	. . . . . . 7 ⊢ (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
105		resundi 5945	. . . . . . 7 ⊢ (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
106	104, 105	eqtri 2762	. . . . . 6 ⊢ (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
107		dmres 5964	. . . . . . . . 9 ⊢ dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
108	42	eqeq1i 2744	. . . . . . . . . . . 12 ⊢ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 ↔ ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} = dom 𝑈)
109	108	bilani 505	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} = dom 𝑈)
110	35	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ∈ No )
111	7	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 ∈ No )
112		simp23 1215	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → 𝑍 ∈ No )
113		sonr 5550	. . . . . . . . . . . . . . . . . 18 ⊢ (( <s Or No ∧ 𝑍 ∈ No ) → ¬ 𝑍 <s 𝑍)
114	95, 112, 113	sylancr 593	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑍 <s 𝑍)
115		breq2 5076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 = 𝑍 → (𝑍 <s 𝑈 ↔ 𝑍 <s 𝑍))
116	115	notbid 319	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 = 𝑍 → (¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍))
117	114, 116	syl5ibrcom 248	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → (𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈))
118	117	necon2ad 2949	. . . . . . . . . . . . . . 15 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → (𝑍 <s 𝑈 → 𝑈 ≠ 𝑍))
119	118	imp 407	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ≠ 𝑍)
120	119	necomd 2989	. . . . . . . . . . . . 13 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 ≠ 𝑈)
121	120	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ≠ 𝑈)
122		nosepssdm 27668	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ No ∧ 𝑈 ∈ No ∧ 𝑍 ≠ 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍)
123	110, 111, 121, 122	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍)
124	109, 123	eqsstrrd 3950	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
125		dfss2 3901	. . . . . . . . . 10 ⊢ (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
126	124, 125	sylib 219	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
127	107, 126	eqtrid 2786	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
128	127	eleq2d 2825	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
129		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
130	129	fvresd 6847	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞))
131	111, 8	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ On)
132		onelon 6335	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
133	131, 132	sylan 586	. . . . . . . . . . . . . 14 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
134		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)
135	134	eleq2d 2825	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ↔ 𝑞 ∈ dom 𝑈))
136	135	biimpar 478	. . . . . . . . . . . . . 14 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})
137	133, 136, 25	sylc 65	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
138		nesym 2990	. . . . . . . . . . . . . 14 ⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑍‘𝑞) = (𝑈‘𝑞))
139	138	con2bii 358	. . . . . . . . . . . . 13 ⊢ ((𝑍‘𝑞) = (𝑈‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))
140	137, 139	sylibr 235	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍‘𝑞) = (𝑈‘𝑞))
141	130, 140	eqtrd 2774	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
142	141	ex 413	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))
143	128, 142	sylbid 241	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))
144	143	ralrimiv 3130	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))
145		nofun 27631	. . . . . . . . . . 11 ⊢ (𝑍 ∈ No → Fun 𝑍)
146	110, 145	syl 17	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑍)
147	146	funresd 6528	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈))
148	64	adantr 481	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑈)
149		eqfunfv 6977	. . . . . . . . 9 ⊢ ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))))
150	147, 148, 149	syl2anc 590	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))))
151	127, 144, 150	mpbir2and 719	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈)
152	35, 145	syl 17	. . . . . . . . . 10 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑍)
153	152	funfnd 6516	. . . . . . . . 9 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 Fn dom 𝑍)
154		ndmfv 6859	. . . . . . . . . . . . . . . 16 ⊢ (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
155		2on0 8409	. . . . . . . . . . . . . . . . . . 19 ⊢ 2_o ≠ ∅
156	155	necomi 2988	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ≠ 2_o
157		neeq1 2996	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈‘dom 𝑈) = ∅ → ((𝑈‘dom 𝑈) ≠ 2_o ↔ ∅ ≠ 2_o))
158	156, 157	mpbiri 259	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘dom 𝑈) = ∅ → (𝑈‘dom 𝑈) ≠ 2_o)
159	158	neneqd 2939	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈‘dom 𝑈) = ∅ → ¬ (𝑈‘dom 𝑈) = 2_o)
160	154, 159	syl 17	. . . . . . . . . . . . . . 15 ⊢ (¬ dom 𝑈 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑈) = 2_o)
161	111, 70, 73, 160	4syl 19	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 2_o)
162	161	intnand 489	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2_o))
163		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 <s 𝑈)
164	35, 7, 37	syl2anc 590	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})))
165	163, 164	mpbid 233	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))
166	165	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))
167	109	fveq2d 6831	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) = (𝑍‘dom 𝑈))
168	109	fveq2d 6831	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) = (𝑈‘dom 𝑈))
169	166, 167, 168	3brtr3d 5103	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈){⟨1_o, ∅⟩, ⟨1_o, 2_o⟩, ⟨∅, 2_o⟩} (𝑈‘dom 𝑈))
170		fvex 6840	. . . . . . . . . . . . . . 15 ⊢ (𝑍‘dom 𝑈) ∈ V
171		fvex 6840	. . . . . . . . . . . . . . 15 ⊢ (𝑈‘dom 𝑈) ∈ V
172	170, 171	brtp 5465	. . . . . . . . . . . . . 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 219	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2_o)))
174		3orel3 1494	. . . . . . . . . . . . 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 65	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o)))
176		andi 1015	. . . . . . . . . . . 12 ⊢ (((𝑍‘dom 𝑈) = 1_o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2_o)) ↔ (((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1_o ∧ (𝑈‘dom 𝑈) = 2_o)))
177	175, 176	sylibr 235	. . . . . . . . . . 11 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍‘dom 𝑈) = 1_o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2_o)))
178	177	simpld 495	. . . . . . . . . 10 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 1_o)
179		ndmfv 6859	. . . . . . . . . . . 12 ⊢ (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
180		1n0 8413	. . . . . . . . . . . . . . 15 ⊢ 1_o ≠ ∅
181	180	necomi 2988	. . . . . . . . . . . . . 14 ⊢ ∅ ≠ 1_o
182		neeq1 2996	. . . . . . . . . . . . . 14 ⊢ ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 1_o ↔ ∅ ≠ 1_o))
183	181, 182	mpbiri 259	. . . . . . . . . . . . 13 ⊢ ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 1_o)
184	183	neneqd 2939	. . . . . . . . . . . 12 ⊢ ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 1_o)
185	179, 184	syl 17	. . . . . . . . . . 11 ⊢ (¬ dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 1_o)
186	185	con4i 114	. . . . . . . . . 10 ⊢ ((𝑍‘dom 𝑈) = 1_o → dom 𝑈 ∈ dom 𝑍)
187	178, 186	syl 17	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍)
188		fnressn 7101	. . . . . . . . 9 ⊢ ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
189	153, 187, 188	syl2an2r 691	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
190	178	opeq2d 4811	. . . . . . . . 9 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 1_o⟩)
191	190	sneqd 4567	. . . . . . . 8 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 1_o⟩})
192	189, 191	eqtrd 2774	. . . . . . 7 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 1_o⟩})
193	151, 192	uneq12d 4099	. . . . . 6 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
194	106, 193	eqtrid 2786	. . . . 5 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}))
195	194	breq2d 5084	. . . 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 326	. . 3 ⊢ (((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))
197		nosepssdm 27668	. . . . 5 ⊢ ((𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈)
198	7, 35, 119, 197	syl3anc 1379	. . . 4 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈)
199		nosepon 27647	. . . . . 6 ⊢ ((𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
200	7, 35, 119, 199	syl3anc 1379	. . . . 5 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On)
201		onsseleq 6351	. . . . 5 ⊢ ((∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)))
202	200, 9, 201	syl2anc 590	. . . 4 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)))
203	198, 202	mpbid 233	. . 3 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))
204	99, 196, 203	mpjaodan 966	. 2 ⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))
205	4, 204	mpdan 693	1 ⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 ∨ w3o 1091 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 {crab 3391 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4261 {csn 4555 {ctp 4559 ⟨cop 4561 ∩ cint 4877 class class class wbr 5072 Or wor 5525 dom cdm 5618 ↾ cres 5620 Rel wrel 5623 Ord word 6309 Oncon0 6310 suc csuc 6312 Fun wfun 6479 Fn wfn 6480 ‘cfv 6485 1_oc1o 8388 2_oc2o 8389 No csur 27621 <s clts 27622

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-ord 6313 df-on 6314 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-1o 8395 df-2o 8396 df-no 27624 df-lts 27625

This theorem is referenced by: noinfbnd2 27713

W3C validator