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 4475	. . . . 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 2783	. . . 4 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → 𝑇 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
4	3	fveq1d 6842	. . 3 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (𝑇‘𝐺) = ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))‘𝐺))
5	4	3ad2ant1 1134	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇‘𝐺) = ((𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))‘𝐺))
6		dmeq 5858	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → dom 𝑢 = dom 𝑈)
7	6	eleq2d 2822	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑈))
8		breq1 5088	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑢 <s 𝑣 ↔ 𝑈 <s 𝑣))
9	8	notbid 318	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑈 <s 𝑣))
10		reseq1 5938	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑢 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
11	10	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
12	9, 11	imbi12d 344	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
13	12	ralbidv 3160	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
14	7, 13	anbi12d 633	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
15	14	rspcev 3564	. . . . . 6 ⊢ ((𝑈 ∈ 𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
16	15	3impb 1115	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
17	16	3ad2ant3 1136	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
18		simp32 1212	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑈)
19		eleq1 2824	. . . . . . . 8 ⊢ (𝑦 = 𝐺 → (𝑦 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑢))
20		suceq 6391	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐺 → suc 𝑦 = suc 𝐺)
21	20	reseq2d 5944	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐺 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝐺))
22	20	reseq2d 5944	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐺 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝐺))
23	21, 22	eqeq12d 2752	. . . . . . . . . 10 ⊢ (𝑦 = 𝐺 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
24	23	imbi2d 340	. . . . . . . . 9 ⊢ (𝑦 = 𝐺 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
25	24	ralbidv 3160	. . . . . . . 8 ⊢ (𝑦 = 𝐺 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
26	19, 25	anbi12d 633	. . . . . . 7 ⊢ (𝑦 = 𝐺 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
27	26	rexbidv 3161	. . . . . 6 ⊢ (𝑦 = 𝐺 → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
28	27	elabg 3619	. . . . 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 2824	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑢))
32		suceq 6391	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → suc 𝑔 = suc 𝐺)
33	32	reseq2d 5944	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑢 ↾ suc 𝑔) = (𝑢 ↾ suc 𝐺))
34	32	reseq2d 5944	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑣 ↾ suc 𝑔) = (𝑣 ↾ suc 𝐺))
35	33, 34	eqeq12d 2752	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
36	35	imbi2d 340	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
37	36	ralbidv 3160	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
38		fveqeq2 6849	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑢‘𝑔) = 𝑥 ↔ (𝑢‘𝐺) = 𝑥))
39	31, 37, 38	3anbi123d 1439	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
40	39	rexbidv 3161	. . . . 5 ⊢ (𝑔 = 𝐺 → (∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥) ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
41	40	iotabidv 6482	. . . 4 ⊢ (𝑔 = 𝐺 → (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) = (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
42		eqid 2736	. . . 4 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
43		iotaex 6474	. . . 4 ⊢ (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) ∈ V
44	41, 42, 43	fvmpt 6947	. . 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 1137	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝑈 ∈ 𝐵)
47		simp2 1138	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝐺 ∈ dom 𝑈)
48		simp3 1139	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
49		eqidd 2737	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → (𝑈‘𝐺) = (𝑈‘𝐺))
50		fveq1 6839	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝑢‘𝐺) = (𝑈‘𝐺))
51	50	eqeq1d 2738	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑢‘𝐺) = (𝑈‘𝐺) ↔ (𝑈‘𝐺) = (𝑈‘𝐺)))
52	7, 13, 51	3anbi123d 1439	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑈‘𝐺) = (𝑈‘𝐺))))
53	52	rspcev 3564	. . . . 5 ⊢ ((𝑈 ∈ 𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑈‘𝐺) = (𝑈‘𝐺))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)))
54	46, 47, 48, 49, 53	syl13anc 1375	. . . 4 ⊢ ((𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)))
55	54	3ad2ant3 1136	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)))
56		fvex 6853	. . . 4 ⊢ (𝑈‘𝐺) ∈ V
57		eqid 2736	. . . . . . . . . 10 ⊢ (𝑢‘𝐺) = (𝑢‘𝐺)
58		fvex 6853	. . . . . . . . . . 11 ⊢ (𝑢‘𝐺) ∈ V
59		eqeq2 2748	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑢‘𝐺) → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = (𝑢‘𝐺)))
60	59	3anbi3d 1445	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑢‘𝐺) → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑢‘𝐺))))
61	58, 60	spcev 3548	. . . . . . . . . 10 ⊢ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑢‘𝐺)) → ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
62	57, 61	mp3an3 1453	. . . . . . . . 9 ⊢ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
63	62	reximi 3075	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢 ∈ 𝐵 ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
64		rexcom4 3264	. . . . . . . 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 1136	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
68		simp2l 1201	. . . . . 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 2569	. . . . 5 ⊢ (∃!𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (∃𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃*𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)))
72	67, 70, 71	sylanbrc 584	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃!𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
73		eqeq2 2748	. . . . . . 7 ⊢ (𝑥 = (𝑈‘𝐺) → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = (𝑈‘𝐺)))
74	73	3anbi3d 1445	. . . . . 6 ⊢ (𝑥 = (𝑈‘𝐺) → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺))))
75	74	rexbidv 3161	. . . . 5 ⊢ (𝑥 = (𝑈‘𝐺) → (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺))))
76	75	iota2 6487	. . . 4 ⊢ (((𝑈‘𝐺) ∈ V ∧ ∃!𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) → (∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = (𝑈‘𝐺)) ↔ (℩𝑥∃𝑢 ∈ 𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) = (𝑈‘𝐺)))
77	56, 72, 76	sylancr 588	. . 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 2775	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇‘𝐺) = (𝑈‘𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∃*wmo 2537 ∃!weu 2568 {cab 2714 ∀wral 3051 ∃wrex 3061 Vcvv 3429 ∪ cun 3887 ⊆ wss 3889 ifcif 4466 {csn 4567 ⟨cop 4573 class class class wbr 5085 ↦ cmpt 5166 dom cdm 5631 ↾ cres 5633 suc csuc 6325 ℩cio 6452 ‘cfv 6498 ℩crio 7323 1_oc1o 8398 No csur 27603 <s clts 27604

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pr 5375

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-ord 6326 df-on 6327 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-fv 6506 df-1o 8405 df-2o 8406 df-no 27606 df-lts 27607

This theorem is referenced by: noinfres 27686

W3C validator