Theorem nosupno 32812

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

Hypothesis

Ref	Expression
nosupno.1	⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))

Assertion

Ref	Expression
nosupno	⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → 𝑆 ∈ No )

Distinct variable group:   𝑥,𝐴,𝑦,𝑔,𝑣,𝑢

Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢,𝑔)

Proof of Theorem nosupno

Dummy variables 𝑎 𝑏 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3455	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		nosupno.1	. . 3 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
3		iftrue 4387	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
4	3	adantr 481	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
5		simprl 767	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → 𝐴 ⊆ No )
6		simpl 483	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
7		nomaxmo 32810	. . . . . . . . . 10 ⊢ (𝐴 ⊆ No → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
8	7	ad2antrl 724	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
9		reu5 3390	. . . . . . . . 9 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
10	6, 8, 9	sylanbrc 583	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
11		riotacl 6991	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
12	10, 11	syl 17	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
13	5, 12	sseldd 3890	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
14		2on 7962	. . . . . . . . 9 ⊢ 2o ∈ On
15	14	elexi 3456	. . . . . . . 8 ⊢ 2o ∈ V
16	15	prid2 4606	. . . . . . 7 ⊢ 2o ∈ {1o, 2o}
17	16	noextend 32782	. . . . . 6 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
18	13, 17	syl 17	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
19	4, 18	eqeltrd 2883	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) ∈ No )
20		iffalse 4390	. . . . . 6 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
21	20	adantr 481	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
22		funmpt 6263	. . . . . . 7 ⊢ Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
23	22	a1i 11	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
24		iotaex 6206	. . . . . . . . 9 ⊢ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ∈ V
25		eqid 2795	. . . . . . . . 9 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
26	24, 25	dmmpti 6360	. . . . . . . 8 ⊢ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
27		ssel2 3884	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ No )
28		nodmon 32766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ No → dom 𝑢 ∈ On)
29	27, 28	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ∈ On)
30		onss 7361	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑢 ∈ On → dom 𝑢 ⊆ On)
31	29, 30	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ⊆ On)
32	31	sseld 3888	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → (𝑦 ∈ dom 𝑢 → 𝑦 ∈ On))
33	32	adantrd 492	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
34	33	rexlimdva 3247	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ No → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
35	34	abssdv 3966	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ No → {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On)
36		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) → 𝑎 ∈ 𝑏)
37	29	adantlr 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ∈ On)
38		ontr1 6112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom 𝑢 ∈ On → ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) → ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
40	36, 39	mpand 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) → (𝑏 ∈ dom 𝑢 → 𝑎 ∈ dom 𝑢))
41	40	adantrd 492	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → 𝑎 ∈ dom 𝑢))
42		reseq1 5728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎))
43		onelon 6091	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((dom 𝑢 ∈ On ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
44	37, 43	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
45		suceloni 7384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∈ On → suc 𝑏 ∈ On)
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑏 ∈ On)
47		simpllr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑎 ∈ 𝑏)
48		eloni 6076	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ On → Ord 𝑏)
49	44, 48	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → Ord 𝑏)
50		ordsucelsuc 7393	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑏 → (𝑎 ∈ 𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → (𝑎 ∈ 𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
52	47, 51	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ∈ suc 𝑏)
53		onelss 6108	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑏 ∈ On → (suc 𝑎 ∈ suc 𝑏 → suc 𝑎 ⊆ suc 𝑏))
54	46, 52, 53	sylc 65	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ⊆ suc 𝑏)
55	54	resabs1d 5765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑢 ↾ suc 𝑎))
56	54	resabs1d 5765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
57	55, 56	eqeq12d 2810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → (((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
58	42, 57	syl5ib 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
59	58	imim2d 57	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
60	59	ralimdv 3145	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) ∧ 𝑏 ∈ dom 𝑢) → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
61	60	expimpd 454	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
62	41, 61	jcad 513	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) ∧ 𝑢 ∈ 𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
63	62	reximdva 3237	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ No ∧ 𝑎 ∈ 𝑏) → (∃𝑢 ∈ 𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∃𝑢 ∈ 𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
64	63	expimpd 454	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ No → ((𝑎 ∈ 𝑏 ∧ ∃𝑢 ∈ 𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))) → ∃𝑢 ∈ 𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
65		vex 3440	. . . . . . . . . . . . . . . 16 ⊢ 𝑏 ∈ V
66		eleq1w 2865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑏 → (𝑦 ∈ dom 𝑢 ↔ 𝑏 ∈ dom 𝑢))
67		suceq 6131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑏 → suc 𝑦 = suc 𝑏)
68	67	reseq2d 5734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑏))
69	67	reseq2d 5734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑏 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑏))
70	68, 69	eqeq12d 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑏 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))
71	70	imbi2d 342	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑏 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
72	71	ralbidv 3164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑏 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
73	66, 72	anbi12d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑏 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
74	73	rexbidv 3260	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑏 → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
75	65, 74	elab 3605	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
76	75	anbi2i 622	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) ↔ (𝑎 ∈ 𝑏 ∧ ∃𝑢 ∈ 𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
77		vex 3440	. . . . . . . . . . . . . . 15 ⊢ 𝑎 ∈ V
78		eleq1w 2865	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑎 → (𝑦 ∈ dom 𝑢 ↔ 𝑎 ∈ dom 𝑢))
79		suceq 6131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑎 → suc 𝑦 = suc 𝑎)
80	79	reseq2d 5734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑎 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑎))
81	79	reseq2d 5734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑎 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑎))
82	80, 81	eqeq12d 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑎 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
83	82	imbi2d 342	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑎 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
84	83	ralbidv 3164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑎 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
85	78, 84	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑎 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
86	85	rexbidv 3260	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
87	77, 86	elab 3605	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
88	64, 76, 87	3imtr4g 297	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ No → ((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
89	88	alrimivv 1906	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ No → ∀𝑎∀𝑏((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
90		dftr2 5065	. . . . . . . . . . . 12 ⊢ (Tr {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∀𝑎∀𝑏((𝑎 ∈ 𝑏 ∧ 𝑏 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
91	89, 90	sylibr 235	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ No → Tr {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
92		dford5 32565	. . . . . . . . . . 11 ⊢ (Ord {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ({𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On ∧ Tr {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
93	35, 91, 92	sylanbrc 583	. . . . . . . . . 10 ⊢ (𝐴 ⊆ No → Ord {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
94	93	adantr 481	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → Ord {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
95		bdayfo 32791	. . . . . . . . . . . . . . 15 ⊢ bday : No –onto→On
96		fofun 6459	. . . . . . . . . . . . . . 15 ⊢ ( bday : No –onto→On → Fun bday )
97	95, 96	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Fun bday
98		funimaexg 6310	. . . . . . . . . . . . . 14 ⊢ ((Fun bday ∧ 𝐴 ∈ V) → ( bday “ 𝐴) ∈ V)
99	97, 98	mpan 686	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ V → ( bday “ 𝐴) ∈ V)
100		uniexg 7325	. . . . . . . . . . . . 13 ⊢ (( bday “ 𝐴) ∈ V → ∪ ( bday “ 𝐴) ∈ V)
101	99, 100	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → ∪ ( bday “ 𝐴) ∈ V)
102	101	adantl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ∪ ( bday “ 𝐴) ∈ V)
103		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ dom 𝑢)
104	103	reximi 3207	. . . . . . . . . . . . 13 ⊢ (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → ∃𝑢 ∈ 𝐴 𝑦 ∈ dom 𝑢)
105	104	ss2abi 3964	. . . . . . . . . . . 12 ⊢ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ {𝑦 ∣ ∃𝑢 ∈ 𝐴 𝑦 ∈ dom 𝑢}
106		bdayval 32764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ No → ( bday ‘𝑢) = dom 𝑢)
107	27, 106	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) = dom 𝑢)
108		fofn 6460	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( bday : No –onto→On → bday Fn No )
109	95, 108	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ bday Fn No
110		fnfvima 6860	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
111	109, 110	mp3an1 1440	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
112	107, 111	eqeltrrd 2884	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ∈ ( bday “ 𝐴))
113		elssuni 4774	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑢 ∈ ( bday “ 𝐴) → dom 𝑢 ⊆ ∪ ( bday “ 𝐴))
114	112, 113	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ⊆ ∪ ( bday “ 𝐴))
115	114	sseld 3888	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → (𝑦 ∈ dom 𝑢 → 𝑦 ∈ ∪ ( bday “ 𝐴)))
116	115	rexlimdva 3247	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ No → (∃𝑢 ∈ 𝐴 𝑦 ∈ dom 𝑢 → 𝑦 ∈ ∪ ( bday “ 𝐴)))
117	116	abssdv 3966	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ No → {𝑦 ∣ ∃𝑢 ∈ 𝐴 𝑦 ∈ dom 𝑢} ⊆ ∪ ( bday “ 𝐴))
118	117	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢 ∈ 𝐴 𝑦 ∈ dom 𝑢} ⊆ ∪ ( bday “ 𝐴))
119	105, 118	syl5ss 3900	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ ∪ ( bday “ 𝐴))
120	102, 119	ssexd 5119	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V)
121		elong 6074	. . . . . . . . . 10 ⊢ ({𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V → ({𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
122	120, 121	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ({𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
123	94, 122	mpbird 258	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On)
124	26, 123	syl5eqel 2887	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∈ On)
125	124	adantl 482	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∈ On)
126	25	rnmpt 5709	. . . . . . . 8 ⊢ ran (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))}
127		vex 3440	. . . . . . . . . . . 12 ⊢ 𝑔 ∈ V
128		eleq1w 2865	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑔 → (𝑦 ∈ dom 𝑢 ↔ 𝑔 ∈ dom 𝑢))
129		suceq 6131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑔 → suc 𝑦 = suc 𝑔)
130	129	reseq2d 5734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑔 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑔))
131	129	reseq2d 5734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑔 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑔))
132	130, 131	eqeq12d 2810	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑔 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
133	132	imbi2d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑔 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
134	133	ralbidv 3164	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑔 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
135	128, 134	anbi12d 630	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑔 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
136	135	rexbidv 3260	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑔 → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
137	127, 136	elab 3605	. . . . . . . . . . 11 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
138		eqid 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢‘𝑔) = (𝑢‘𝑔)
139		fvex 6551	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢‘𝑔) ∈ V
140		eqeq2 2806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑢‘𝑔) → ((𝑢‘𝑔) = 𝑥 ↔ (𝑢‘𝑔) = (𝑢‘𝑔)))
141	140	3anbi3d 1434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑢‘𝑔) → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = (𝑢‘𝑔))))
142	139, 141	spcev 3549	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = (𝑢‘𝑔)) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
143	138, 142	mp3an3 1442	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
144	143	reximi 3207	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑢 ∈ 𝐴 ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
145		rexcom4 3213	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝐴 ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ ∃𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
146	144, 145	sylib 219	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
147	146	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ No ∧ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
148		noprefixmo 32811	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
149	148	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ No ∧ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃*𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
150		df-eu 2612	. . . . . . . . . . . . . . 15 ⊢ (∃!𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (∃𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ∧ ∃*𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
151	147, 149, 150	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ No ∧ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃!𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
152		vex 3440	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
153		eqeq2 2806	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → ((𝑢‘𝑔) = 𝑥 ↔ (𝑢‘𝑔) = 𝑧))
154	153	3anbi3d 1434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧)))
155	154	rexbidv 3260	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧)))
156	155	iota2 6215	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ V ∧ ∃!𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) → (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧))
157	152, 156	mpan 686	. . . . . . . . . . . . . 14 ⊢ (∃!𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) → (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧))
158	151, 157	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧))
159		eqcom 2802	. . . . . . . . . . . . 13 ⊢ ((℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = 𝑧 ↔ 𝑧 = (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
160	158, 159	syl6bb 288	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) ↔ 𝑧 = (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
161		simprr3 1216	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → (𝑢‘𝑔) = 𝑧)
162	27	adantrr 713	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝑢 ∈ No )
163		norn 32767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ No → ran 𝑢 ⊆ {1o, 2o})
164	162, 163	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → ran 𝑢 ⊆ {1o, 2o})
165		nofun 32765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ No → Fun 𝑢)
166	162, 165	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → Fun 𝑢)
167		simprr1 1214	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝑔 ∈ dom 𝑢)
168		fvelrn 6709	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑢 ∧ 𝑔 ∈ dom 𝑢) → (𝑢‘𝑔) ∈ ran 𝑢)
169	166, 167, 168	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → (𝑢‘𝑔) ∈ ran 𝑢)
170	164, 169	sseldd 3890	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → (𝑢‘𝑔) ∈ {1o, 2o})
171	161, 170	eqeltrrd 2884	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧))) → 𝑧 ∈ {1o, 2o})
172	171	rexlimdvaa 3248	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ No → (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) → 𝑧 ∈ {1o, 2o}))
173	172	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑧) → 𝑧 ∈ {1o, 2o}))
174	160, 173	sylbird 261	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑧 = (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
175	137, 174	sylan2b 593	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ 𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → (𝑧 = (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
176	175	rexlimdva 3247	. . . . . . . . 9 ⊢ (𝐴 ⊆ No → (∃𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
177	176	abssdv 3966	. . . . . . . 8 ⊢ (𝐴 ⊆ No → {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))} ⊆ {1o, 2o})
178	126, 177	syl5eqss 3936	. . . . . . 7 ⊢ (𝐴 ⊆ No → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ⊆ {1o, 2o})
179	178	ad2antrl 724	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ⊆ {1o, 2o})
180		elno2 32770	. . . . . 6 ⊢ ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ 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 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ⊆ {1o, 2o}))
181	23, 125, 179, 180	syl3anbrc 1336	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) ∈ No )
182	21, 181	eqeltrd 2883	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) ∈ No )
183	19, 182	pm2.61ian 808	. . 3 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) ∈ No )
184	2, 183	syl5eqel 2887	. 2 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
185	1, 184	sylan2 592	1 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → 𝑆 ∈ No )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080  ∀wal 1520   = wceq 1522  ∃wex 1761   ∈ wcel 2081  ∃*wmo 2574  ∃!weu 2611  {cab 2775  ∀wral 3105  ∃wrex 3106  ∃!wreu 3107  ∃*wrmo 3108  Vcvv 3437   ∪ cun 3857   ⊆ wss 3859  ifcif 4381  {csn 4472  {cpr 4474  ⟨cop 4478  ∪ cuni 4745   class class class wbr 4962   ↦ cmpt 5041  Tr wtr 5063  dom cdm 5443  ran crn 5444   ↾ cres 5445   “ cima 5446  Ord word 6065  Oncon0 6066  suc csuc 6068  ℩cio 6187  Fun wfun 6219   Fn wfn 6220  –onto→wfo 6223  ‘cfv 6225  ℩crio 6976  1_oc1o 7946  2_oc2o 7947   No csur 32756   <s cslt 32757   bday cbday 32758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-ord 6069  df-on 6070  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-1o 7953  df-2o 7954  df-no 32759  df-slt 32760  df-bday 32761

This theorem is referenced by:  nosupbday  32814  nosupres  32816  nosupbnd1lem1  32817  nosupbnd1lem2  32818  nosupbnd1lem3  32819  nosupbnd1lem4  32820  nosupbnd1lem5  32821  nosupbnd1lem6  32822  nosupbnd2  32825  noetalem1  32826  noetalem2  32827  noetalem3  32828  noetalem4  32829