noinfno - Metamath Proof Explorer

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

Theorem noinfno 27781

Description: The next several theorems deal with a surreal "infimum". This surreal will ultimately be shown to bound 𝐵 above and bound the restriction of any surreal below. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 8-Aug-2024.)

**Hypothesis**
Ref	Expression
noinfno.1	⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))

**Assertion**
Ref	Expression
noinfno	⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )

Distinct variable groups: 𝑥,𝐵,𝑦,𝑔,𝑣,𝑢 𝑔,𝑉 Allowed substitution hints: 𝑇(𝑥,𝑦,𝑣,𝑢,𝑔) 𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfno Dummy variables 𝑎 𝑏 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noinfno.1	. 2 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2		iftrue 4554	. . . . 5 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}))
3	2	adantr 480	. . . 4 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}))
4		simprl 770	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → 𝐵 ⊆ No )
5		simpl 482	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
6		nominmo 27762	. . . . . . . . 9 ⊢ (𝐵 ⊆ No → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
7	6	ad2antrl 727	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
8		reu5 3390	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
9	5, 7, 8	sylanbrc 582	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
10		riotacl 7422	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
11	9, 10	syl 17	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
12	4, 11	sseldd 4009	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ No )
13		1oex 8532	. . . . . . 7 ⊢ 1_o ∈ V
14	13	prid1 4787	. . . . . 6 ⊢ 1_o ∈ {1_o, 2_o}
15	14	noextend 27729	. . . . 5 ⊢ ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}) ∈ No )
16	12, 15	syl 17	. . . 4 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}) ∈ No )
17	3, 16	eqeltrd 2844	. . 3 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) ∈ No )
18		iffalse 4557	. . . . 5 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
19	18	adantr 480	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
20		funmpt 6616	. . . . . 6 ⊢ Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
21	20	a1i 11	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
22		iotaex 6546	. . . . . . 7 ⊢ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ∈ V
23		eqid 2740	. . . . . . 7 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
24	22, 23	dmmpti 6724	. . . . . 6 ⊢ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
25		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → 𝐵 ⊆ No )
26		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → 𝑢 ∈ 𝐵)
27	25, 26	sseldd 4009	. . . . . . . . . . . . 13 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → 𝑢 ∈ No )
28		nodmon 27713	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ No → dom 𝑢 ∈ On)
29	27, 28	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → dom 𝑢 ∈ On)
30		simprrl 780	. . . . . . . . . . . 12 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → 𝑦 ∈ dom 𝑢)
31		onelon 6420	. . . . . . . . . . . 12 ⊢ ((dom 𝑢 ∈ On ∧ 𝑦 ∈ dom 𝑢) → 𝑦 ∈ On)
32	29, 30, 31	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → 𝑦 ∈ On)
33	32	rexlimdvaa 3162	. . . . . . . . . 10 ⊢ (𝐵 ⊆ No → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
34	33	abssdv 4091	. . . . . . . . 9 ⊢ (𝐵 ⊆ No → {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On)
35		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → 𝑎 ∈ 𝑏)
36		ssel2 4003	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ⊆ No ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ No )
37	36	adantlr 714	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ No )
38	37, 28	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → dom 𝑢 ∈ On)
39		ontr1 6441	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑢 ∈ On → ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
41	35, 40	mpand 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → (𝑏 ∈ dom 𝑢 → 𝑎 ∈ dom 𝑢))
42	41	adantrd 491	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → 𝑎 ∈ dom 𝑢))
43		reseq1 6003	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎))
44		onelon 6420	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((dom 𝑢 ∈ On ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
45	38, 44	sylan 579	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
46		onsucb 7853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ On ↔ suc 𝑏 ∈ On)
47	45, 46	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑏 ∈ On)
48		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → 𝑎 ∈ 𝑏)
49		eloni 6405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∈ On → Ord 𝑏)
50	45, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → Ord 𝑏)
51		ordsucelsuc 7858	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝑏 → (𝑎 ∈ 𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → (𝑎 ∈ 𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
53	48, 52	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ∈ suc 𝑏)
54		onelss 6437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑏 ∈ On → (suc 𝑎 ∈ suc 𝑏 → suc 𝑎 ⊆ suc 𝑏))
55	47, 53, 54	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ⊆ suc 𝑏)
56	55	resabs1d 6037	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑢 ↾ suc 𝑎))
57	55	resabs1d 6037	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
58	56, 57	eqeq12d 2756	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → (((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
59	43, 58	imbitrid 244	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
60	59	imim2d 57	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
61	60	ralimdv 3175	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) ∧ 𝑏 ∈ dom 𝑢) → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
62	61	expimpd 453	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
63	42, 62	jcad 512	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐵) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
64	63	reximdva 3174	. . . . . . . . . . . . 13 ⊢ ((𝐵 ⊆ No ∧ 𝑎 ∈ 𝑏) → (∃𝑢 ∈ 𝐵 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∃𝑢 ∈ 𝐵 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
65	64	expimpd 453	. . . . . . . . . . . 12 ⊢ (𝐵 ⊆ No → ((𝑎 ∈ 𝑏 ∧ ∃𝑢 ∈ 𝐵 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))) → ∃𝑢 ∈ 𝐵 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
66		vex 3492	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
67		eleq1w 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → (𝑦 ∈ dom 𝑢 ↔ 𝑏 ∈ dom 𝑢))
68		suceq 6461	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑏 → suc 𝑦 = suc 𝑏)
69	68	reseq2d 6009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑏 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑏))
70	68	reseq2d 6009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑏 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑏))
71	69, 70	eqeq12d 2756	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑏 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))
72	71	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑏 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
73	72	ralbidv 3184	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
74	67, 73	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑏 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
75	74	rexbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐵 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
76	66, 75	elab 3694	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐵 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
77	76	anbi2i 622	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) ↔ (𝑎 ∈ 𝑏 ∧ ∃𝑢 ∈ 𝐵 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
78		vex 3492	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
79		eleq1w 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝑦 ∈ dom 𝑢 ↔ 𝑎 ∈ dom 𝑢))
80		suceq 6461	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑎 → suc 𝑦 = suc 𝑎)
81	80	reseq2d 6009	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑎 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑎))
82	80	reseq2d 6009	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑎 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑎))
83	81, 82	eqeq12d 2756	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑎 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
84	83	imbi2d 340	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑎 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
85	84	ralbidv 3184	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
86	79, 85	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
87	86	rexbidv 3185	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐵 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
88	78, 87	elab 3694	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐵 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
89	65, 77, 88	3imtr4g 296	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ No → ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
90	89	alrimivv 1927	. . . . . . . . . 10 ⊢ (𝐵 ⊆ No → ∀𝑎∀𝑏((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
91		dftr2 5285	. . . . . . . . . 10 ⊢ (Tr {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∀𝑎∀𝑏((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
92	90, 91	sylibr 234	. . . . . . . . 9 ⊢ (𝐵 ⊆ No → Tr {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
93		dford5 7819	. . . . . . . . 9 ⊢ (Ord {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ({𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On ∧ Tr {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
94	34, 92, 93	sylanbrc 582	. . . . . . . 8 ⊢ (𝐵 ⊆ No → Ord {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
95	94	ad2antrl 727	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → Ord {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
96		bdayfo 27740	. . . . . . . . . . . . . 14 ⊢ bday : No –onto→On
97		fofun 6835	. . . . . . . . . . . . . 14 ⊢ ( bday : No –onto→On → Fun bday )
98	96, 97	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Fun bday
99		funimaexg 6664	. . . . . . . . . . . . 13 ⊢ ((Fun bday ∧ 𝐵 ∈ 𝑉) → ( bday “ 𝐵) ∈ V)
100	98, 99	mpan 689	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → ( bday “ 𝐵) ∈ V)
101	100	uniexd 7777	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑉 → ∪ ( bday “ 𝐵) ∈ V)
102	101	adantl 481	. . . . . . . . . 10 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → ∪ ( bday “ 𝐵) ∈ V)
103	102	adantl 481	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ∪ ( bday “ 𝐵) ∈ V)
104		bdayval 27711	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ No → ( bday ‘𝑢) = dom 𝑢)
105	27, 104	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → ( bday ‘𝑢) = dom 𝑢)
106		fofn 6836	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday : No –onto→On → bday Fn No )
107	96, 106	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ bday Fn No
108		fnfvima 7270	. . . . . . . . . . . . . . . . 17 ⊢ (( bday Fn No ∧ 𝐵 ⊆ No ∧ 𝑢 ∈ 𝐵) → ( bday ‘𝑢) ∈ ( bday “ 𝐵))
109	107, 108	mp3an1 1448	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ 𝑢 ∈ 𝐵) → ( bday ‘𝑢) ∈ ( bday “ 𝐵))
110	109	adantrr 716	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → ( bday ‘𝑢) ∈ ( bday “ 𝐵))
111	105, 110	eqeltrrd 2845	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → dom 𝑢 ∈ ( bday “ 𝐵))
112		elssuni 4961	. . . . . . . . . . . . . 14 ⊢ (dom 𝑢 ∈ ( bday “ 𝐵) → dom 𝑢 ⊆ ∪ ( bday “ 𝐵))
113	111, 112	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → dom 𝑢 ⊆ ∪ ( bday “ 𝐵))
114	113, 30	sseldd 4009	. . . . . . . . . . . 12 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))))) → 𝑦 ∈ ∪ ( bday “ 𝐵))
115	114	rexlimdvaa 3162	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ No → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ ∪ ( bday “ 𝐵)))
116	115	abssdv 4091	. . . . . . . . . 10 ⊢ (𝐵 ⊆ No → {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ ∪ ( bday “ 𝐵))
117	116	ad2antrl 727	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ ∪ ( bday “ 𝐵))
118	103, 117	ssexd 5342	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V)
119		elong 6403	. . . . . . . 8 ⊢ ({𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V → ({𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
120	118, 119	syl 17	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ({𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
121	95, 120	mpbird 257	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On)
122	24, 121	eqeltrid 2848	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∈ On)
123	23	rnmpt 5980	. . . . . 6 ⊢ ran (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))}
124		eleq1w 2827	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑔 → (𝑦 ∈ dom 𝑢 ↔ 𝑔 ∈ dom 𝑢))
125		suceq 6461	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑔 → suc 𝑦 = suc 𝑔)
126	125	reseq2d 6009	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑔 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑔))
127	125	reseq2d 6009	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑔 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑔))
128	126, 127	eqeq12d 2756	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑔 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
129	128	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑔 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
130	129	ralbidv 3184	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑔 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
131	124, 130	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑔 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
132	131	rexbidv 3185	. . . . . . . . 9 ⊢ (𝑦 = 𝑔 → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
133	132	rexab 3716	. . . . . . . 8 ⊢ (∃𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ↔ ∃𝑔(∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) ∧ 𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
134		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢‘𝑔) = (𝑢‘𝑔)
135		fvex 6933	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢‘𝑔) ∈ V
136		eqeq2 2752	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑢‘𝑔) → ((𝑢‘𝑔) = 𝑥 ↔ (𝑢‘𝑔) = (𝑢‘𝑔)))
137	136	3anbi3d 1442	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑢‘𝑔) → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = (𝑢‘𝑔))))
138	135, 137	spcev 3619	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = (𝑢‘𝑔)) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
139	134, 138	mp3an3 1450	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
140	139	reximi 3090	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑢 ∈ 𝐵 ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
141		rexcom4 3294	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝐵 ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ ∃𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
142	140, 141	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
143	142	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) ∧ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
144		noinfprefixmo 27764	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
145	144	ad2antrl 727	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ∃*𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
146	145	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) ∧ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃*𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
147		df-eu 2572	. . . . . . . . . . . . . 14 ⊢ (∃!𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (∃𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ∧ ∃*𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
148	143, 146, 147	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) ∧ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃!𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
149		vex 3492	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
150		eqeq2 2752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((𝑢‘𝑔) = 𝑥 ↔ (𝑢‘𝑔) = 𝑧))
151	150	3anbi3d 1442	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧)))
152	151	rexbidv 3185	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧)))
153	152	iota2 6562	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ V ∧ ∃!𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧))
154	149, 153	mpan 689	. . . . . . . . . . . . 13 ⊢ (∃!𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧))
155	148, 154	syl 17	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) ∧ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧))
156		eqcom 2747	. . . . . . . . . . . 12 ⊢ ((℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧 ↔ 𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
157	155, 156	bitrdi 287	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) ∧ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ 𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
158		simprr3 1223	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → (𝑢‘𝑔) = 𝑧)
159		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝐵 ⊆ No )
160		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝑢 ∈ 𝐵)
161	159, 160	sseldd 4009	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝑢 ∈ No )
162		norn 27714	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ No → ran 𝑢 ⊆ {1_o, 2_o})
163	161, 162	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → ran 𝑢 ⊆ {1_o, 2_o})
164		nofun 27712	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ No → Fun 𝑢)
165	161, 164	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → Fun 𝑢)
166		simprr1 1221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝑔 ∈ dom 𝑢)
167		fvelrn 7110	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑢 ∧ 𝑔 ∈ dom 𝑢) → (𝑢‘𝑔) ∈ ran 𝑢)
168	165, 166, 167	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → (𝑢‘𝑔) ∈ ran 𝑢)
169	163, 168	sseldd 4009	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → (𝑢‘𝑔) ∈ {1_o, 2_o})
170	158, 169	eqeltrrd 2845	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ⊆ No ∧ (𝑢 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝑧 ∈ {1_o, 2_o})
171	170	rexlimdvaa 3162	. . . . . . . . . . . . 13 ⊢ (𝐵 ⊆ No → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) → 𝑧 ∈ {1_o, 2_o}))
172	171	ad2antrl 727	. . . . . . . . . . . 12 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) → 𝑧 ∈ {1_o, 2_o}))
173	172	adantr 480	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) ∧ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) → 𝑧 ∈ {1_o, 2_o}))
174	157, 173	sylbird 260	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) ∧ ∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) → 𝑧 ∈ {1_o, 2_o}))
175	174	expimpd 453	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ((∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) ∧ 𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) → 𝑧 ∈ {1_o, 2_o}))
176	175	exlimdv 1932	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → (∃𝑔(∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) ∧ 𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) → 𝑧 ∈ {1_o, 2_o}))
177	133, 176	biimtrid 242	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → (∃𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) → 𝑧 ∈ {1_o, 2_o}))
178	177	abssdv 4091	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))} ⊆ {1_o, 2_o})
179	123, 178	eqsstrid 4057	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ⊆ {1_o, 2_o})
180		elno2 27717	. . . . 5 ⊢ ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∈ No ↔ (Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∧ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∈ On ∧ ran (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ⊆ {1_o, 2_o}))
181	21, 122, 179, 180	syl3anbrc 1343	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∈ No )
182	19, 181	eqeltrd 2844	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉)) → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) ∈ No )
183	17, 182	pm2.61ian 811	. 2 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) ∈ No )
184	1, 183	eqeltrid 2848	1 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 ∀wal 1535 = wceq 1537 ∃wex 1777 ∈ wcel 2108 ∃*wmo 2541 ∃!weu 2571 {cab 2717 ∀wral 3067 ∃wrex 3076 ∃!wreu 3386 ∃*wrmo 3387 Vcvv 3488 ∪ cun 3974 ⊆ wss 3976 ifcif 4548 {csn 4648 {cpr 4650 ⟨cop 4654 ∪ cuni 4931 class class class wbr 5166 ↦ cmpt 5249 Tr wtr 5283 dom cdm 5700 ran crn 5701 ↾ cres 5702 “ cima 5703 Ord word 6394 Oncon0 6395 suc csuc 6397 ℩cio 6523 Fun wfun 6567 Fn wfn 6568 –onto→wfo 6571 ‘cfv 6573 ℩crio 7403 1_oc1o 8515 2_oc2o 8516 No csur 27702 <s cslt 27703 bday cbday 27704

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-ord 6398 df-on 6399 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-fo 6579 df-fv 6581 df-riota 7404 df-1o 8522 df-2o 8523 df-no 27705 df-slt 27706 df-bday 27707

This theorem is referenced by: noinfbday 27783 noinfres 27785 noinfbnd1lem1 27786 noinfbnd1lem2 27787 noinfbnd1lem3 27788 noinfbnd1lem4 27789 noinfbnd1lem5 27790 noinfbnd1lem6 27791 noinfbnd2 27794 nosupinfsep 27795 noetainflem1 27800 noetainflem2 27801 noetainflem3 27802 noetainflem4 27803 noetalem1 27804

W3C validator