noinffv - Metamath Proof Explorer

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

Theorem noinffv 27685

Description: The value of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024.)

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

**Assertion**
Ref	Expression
noinffv	⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇‘𝐺) = (𝑈‘𝐺))

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

**Proof of Theorem noinffv**
Step	Hyp	Ref	Expression
1		noinffv.1	. . . . 5 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2		iffalse 4509	. . . . 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 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
3	1, 2	eqtrid 2782	. . . 4 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → 𝑇 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
4	3	fveq1d 6878	. . 3 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (𝑇‘𝐺) = ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))‘𝐺))
5	4	3ad2ant1 1133	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇‘𝐺) = ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))‘𝐺))
6		dmeq 5883	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → dom 𝑢 = dom 𝑈)
7	6	eleq2d 2820	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑈))
8		breq1 5122	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑢 <s 𝑣 ↔ 𝑈 <s 𝑣))
9	8	notbid 318	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑈 <s 𝑣))
10		reseq1 5960	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑢 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
11	10	eqeq1d 2737	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
12	9, 11	imbi12d 344	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
13	12	ralbidv 3163	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
14	7, 13	anbi12d 632	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
15	14	rspcev 3601	. . . . . 6 ⊢ ((𝑈 ∈ 𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
16	15	3impb 1114	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
17	16	3ad2ant3 1135	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
18		simp32 1211	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑈)
19		eleq1 2822	. . . . . . . 8 ⊢ (𝑦 = 𝐺 → (𝑦 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑢))
20		suceq 6419	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐺 → suc 𝑦 = suc 𝐺)
21	20	reseq2d 5966	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐺 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝐺))
22	20	reseq2d 5966	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐺 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝐺))
23	21, 22	eqeq12d 2751	. . . . . . . . . 10 ⊢ (𝑦 = 𝐺 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
24	23	imbi2d 340	. . . . . . . . 9 ⊢ (𝑦 = 𝐺 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
25	24	ralbidv 3163	. . . . . . . 8 ⊢ (𝑦 = 𝐺 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
26	19, 25	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = 𝐺 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
27	26	rexbidv 3164	. . . . . 6 ⊢ (𝑦 = 𝐺 → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
28	27	elabg 3655	. . . . 5 ⊢ (𝐺 ∈ dom 𝑈 → (𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
29	18, 28	syl 17	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
30	17, 29	mpbird 257	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
31		eleq1 2822	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑢))
32		suceq 6419	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → suc 𝑔 = suc 𝐺)
33	32	reseq2d 5966	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑢 ↾ suc 𝑔) = (𝑢 ↾ suc 𝐺))
34	32	reseq2d 5966	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑣 ↾ suc 𝑔) = (𝑣 ↾ suc 𝐺))
35	33, 34	eqeq12d 2751	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
36	35	imbi2d 340	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
37	36	ralbidv 3163	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
38		fveqeq2 6885	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑢‘𝑔) = 𝑥 ↔ (𝑢‘𝐺) = 𝑥))
39	31, 37, 38	3anbi123d 1438	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
40	39	rexbidv 3164	. . . . 5 ⊢ (𝑔 = 𝐺 → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
41	40	iotabidv 6515	. . . 4 ⊢ (𝑔 = 𝐺 → (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
42		eqid 2735	. . . 4 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
43		iotaex 6504	. . . 4 ⊢ (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) ∈ V
44	41, 42, 43	fvmpt 6986	. . 3 ⊢ (𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} → ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))‘𝐺) = (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
45	30, 44	syl 17	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))‘𝐺) = (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
46		simp1 1136	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝑈 ∈ 𝐵)
47		simp2 1137	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝐺 ∈ dom 𝑈)
48		simp3 1138	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
49		eqidd 2736	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → (𝑈‘𝐺) = (𝑈‘𝐺))
50		fveq1 6875	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝑢‘𝐺) = (𝑈‘𝐺))
51	50	eqeq1d 2737	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑢‘𝐺) = (𝑈‘𝐺) ↔ (𝑈‘𝐺) = (𝑈‘𝐺)))
52	7, 13, 51	3anbi123d 1438	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑈‘𝐺) = (𝑈‘𝐺))))
53	52	rspcev 3601	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑈‘𝐺) = (𝑈‘𝐺))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)))
54	46, 47, 48, 49, 53	syl13anc 1374	. . . 4 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)))
55	54	3ad2ant3 1135	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)))
56		fvex 6889	. . . 4 ⊢ (𝑈‘𝐺) ∈ V
57		eqid 2735	. . . . . . . . . 10 ⊢ (𝑢‘𝐺) = (𝑢‘𝐺)
58		fvex 6889	. . . . . . . . . . 11 ⊢ (𝑢‘𝐺) ∈ V
59		eqeq2 2747	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑢‘𝐺) → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = (𝑢‘𝐺)))
60	59	3anbi3d 1444	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑢‘𝐺) → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑢‘𝐺))))
61	58, 60	spcev 3585	. . . . . . . . . 10 ⊢ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑢‘𝐺)) → ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
62	57, 61	mp3an3 1452	. . . . . . . . 9 ⊢ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
63	62	reximi 3074	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢 ∈ 𝐵 ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
64		rexcom4 3269	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝐵 ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
65	63, 64	sylib 218	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
66	16, 65	syl 17	. . . . . 6 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
67	66	3ad2ant3 1135	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
68		simp2l 1200	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐵 ⊆ No )
69		noinfprefixmo 27665	. . . . . 6 ⊢ (𝐵 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
70	68, 69	syl 17	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃*𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
71		df-eu 2568	. . . . 5 ⊢ (∃!𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (∃𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃*𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
72	67, 70, 71	sylanbrc 583	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃!𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
73		eqeq2 2747	. . . . . . 7 ⊢ (𝑥 = (𝑈‘𝐺) → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = (𝑈‘𝐺)))
74	73	3anbi3d 1444	. . . . . 6 ⊢ (𝑥 = (𝑈‘𝐺) → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺))))
75	74	rexbidv 3164	. . . . 5 ⊢ (𝑥 = (𝑈‘𝐺) → (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺))))
76	75	iota2 6520	. . . 4 ⊢ (((𝑈‘𝐺) ∈ V ∧ ∃!𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) → (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)) ↔ (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) = (𝑈‘𝐺)))
77	56, 72, 76	sylancr 587	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)) ↔ (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) = (𝑈‘𝐺)))
78	55, 77	mpbid 232	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) = (𝑈‘𝐺))
79	5, 45, 78	3eqtrd 2774	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇‘𝐺) = (𝑈‘𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∃*wmo 2537 ∃!weu 2567 {cab 2713 ∀wral 3051 ∃wrex 3060 Vcvv 3459 ∪ cun 3924 ⊆ wss 3926 ifcif 4500 {csn 4601 ⟨cop 4607 class class class wbr 5119 ↦ cmpt 5201 dom cdm 5654 ↾ cres 5656 suc csuc 6354 ℩cio 6482 ‘cfv 6531 ℩crio 7361 1_oc1o 8473 No csur 27603 <s cslt 27604

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-ord 6355 df-on 6356 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-fv 6539 df-1o 8480 df-2o 8481 df-no 27606 df-slt 27607

This theorem is referenced by: noinfres 27686

W3C validator