Theorem ltsval2 28018

Description: Alternate expression for surreal less-than. Two surreals obey surreal less-than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.)

Assertion

Ref	Expression
ltsval2	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))

Distinct variable groups:   𝐴,𝑎   𝐵,𝑎

Proof of Theorem ltsval2

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltsval 28009	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
2		fvex 6898	. . . . . . . . . . . . 13 ⊢ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V
3		fvex 6898	. . . . . . . . . . . . 13 ⊢ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V
4	2, 3	brtp 5496	. . . . . . . . . . . 12 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o)))
5		1n0 8498	. . . . . . . . . . . . . . . . 17 ⊢ 1o ≠ ∅
6	5	neii 2957	. . . . . . . . . . . . . . . 16 ⊢ ¬ 1o = ∅
7		eqeq1 2764	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ↔ 1o = ∅))
8	6, 7	mtbiri 330	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
9		fvprc 6877	. . . . . . . . . . . . . . 15 ⊢ (¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
10	8, 9	nsyl2 142	. . . . . . . . . . . . . 14 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
11	10	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
12	10	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
13		2on0 8494	. . . . . . . . . . . . . . . . 17 ⊢ 2o ≠ ∅
14	13	neii 2957	. . . . . . . . . . . . . . . 16 ⊢ ¬ 2o = ∅
15		eqeq1 2764	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o → ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ↔ 2o = ∅))
16	14, 15	mtbiri 330	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o → ¬ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
17		fvprc 6877	. . . . . . . . . . . . . . 15 ⊢ (¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
18	16, 17	nsyl2 142	. . . . . . . . . . . . . 14 ⊢ ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
19	18	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
20	11, 12, 19	3jaoi 1454	. . . . . . . . . . . 12 ⊢ ((((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
21	4, 20	sylbi 220	. . . . . . . . . . 11 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
22		onintrab 7810	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V ↔ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
23	21, 22	sylib 221	. . . . . . . . . 10 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
24	23	adantl 487	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
25		onelon 6387	. . . . . . . . . . . . . 14 ⊢ ((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑦 ∈ On)
26	25	expcom 419	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On → 𝑦 ∈ On))
27	24, 26	syl5 35	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → 𝑦 ∈ On))
28		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑦 → (𝐴‘𝑎) = (𝐴‘𝑦))
29		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑦 → (𝐵‘𝑎) = (𝐵‘𝑦))
30	28, 29	neeq12d 3016	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑦 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
31	30	onnminsb 7813	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ On → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
32	31	com12 33	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝑦 ∈ On → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
33	27, 32	syldc 49	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
34		df-ne 2956	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑦) ≠ (𝐵‘𝑦) ↔ ¬ (𝐴‘𝑦) = (𝐵‘𝑦))
35	34	con2bii 360	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦))
36	33, 35	imbitrrdi 255	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = (𝐵‘𝑦)))
37	36	ralrimiv 3153	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))
38	24, 37	jca 521	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
39	38	ex 418	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))))
40	39	impac 562	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
41		anass 474	. . . . . 6 ⊢ (((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) ↔ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
42	40, 41	sylib 221	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
43		raleq 3316	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
44		fveq2 6885	. . . . . . . 8 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
45		fveq2 6885	. . . . . . . 8 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
46	44, 45	breq12d 5115	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
47	43, 46	anbi12d 644	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
48	47	rspcev 3576	. . . . 5 ⊢ ((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
49	42, 48	syl 18	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
50	49	ex 418	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
51		eqeq12 2777	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 1o = ∅))
52	6, 51	mtbiri 330	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
53		1on 8492	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ On
54		0elon 6418	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ On
55		suc11 6472	. . . . . . . . . . . . . . . . . 18 ⊢ ((1o ∈ On ∧ ∅ ∈ On) → (suc 1o = suc ∅ ↔ 1o = ∅))
56	55	necon3bid 2999	. . . . . . . . . . . . . . . . 17 ⊢ ((1o ∈ On ∧ ∅ ∈ On) → (suc 1o ≠ suc ∅ ↔ 1o ≠ ∅))
57	53, 54, 56	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (suc 1o ≠ suc ∅ ↔ 1o ≠ ∅)
58	5, 57	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ suc 1o ≠ suc ∅
59		df-2o 8480	. . . . . . . . . . . . . . . 16 ⊢ 2o = suc 1o
60		df-1o 8479	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
61	59, 60	eqeq12i 2778	. . . . . . . . . . . . . . 15 ⊢ (2o = 1o ↔ suc 1o = suc ∅)
62	58, 61	nemtbir 3051	. . . . . . . . . . . . . 14 ⊢ ¬ 2o = 1o
63		eqeq12 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 1o = 2o))
64		eqcom 2767	. . . . . . . . . . . . . . 15 ⊢ (1o = 2o ↔ 2o = 1o)
65	63, 64	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 2o = 1o))
66	62, 65	mtbiri 330	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
67	13	nesymi 3012	. . . . . . . . . . . . . 14 ⊢ ¬ ∅ = 2o
68		eqeq12 2777	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ ∅ = 2o))
69	67, 68	mtbiri 330	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
70	52, 66, 69	3jaoi 1454	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) ∨ ((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) ∨ ((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o)) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
71		fvex 6898	. . . . . . . . . . . . 13 ⊢ (𝐴‘𝑥) ∈ V
72		fvex 6898	. . . . . . . . . . . . 13 ⊢ (𝐵‘𝑥) ∈ V
73	71, 72	brtp 5496	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) ∨ ((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) ∨ ((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o)))
74		df-ne 2956	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
75	70, 73, 74	3imtr4i 295	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) → (𝐴‘𝑥) ≠ (𝐵‘𝑥))
76		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝐴‘𝑎) = (𝐴‘𝑥))
77		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝐵‘𝑎) = (𝐵‘𝑥))
78	76, 77	neeq12d 3016	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝑥) ≠ (𝐵‘𝑥)))
79	78	elrab 3644	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)))
80	79	biimpri 231	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
81	80	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
82		ssrab2 4005	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On
83		ne0i 4286	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅)
84	83	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅)
85		onint 7804	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
86	82, 84, 85	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
87		nfrab1 3431	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}
88	87	nfint 4916	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}
89		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎On
90		nfcv 2922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎𝐴
91	90, 88	nffv 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎(𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
92		nfcv 2922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎𝐵
93	92, 88	nffv 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎(𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
94	91, 93	nfne 3058	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎(𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
95		fveq2 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑎) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
96		fveq2 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑎) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
97	95, 96	neeq12d 3016	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
98	88, 89, 94, 97	elrabf 3641	. . . . . . . . . . . . . . . . . 18 ⊢ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
99	98	simprbi 503	. . . . . . . . . . . . . . . . 17 ⊢ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
100	86, 99	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
101		df-ne 2956	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
102	100, 101	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
103		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
104		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑦) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
105	103, 104	eqeq12d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
106	105	rspccv 3573	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥 → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
107	106	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥 → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
108	102, 107	mtod 201	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥)
109		simpll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 ∈ On)
110		oninton 7809	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
111	82, 83, 110	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
112	111	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
113		ontri1 6397	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) → (𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥))
114	109, 112, 113	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥))
115	108, 114	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
116		intss1 4922	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥)
117	116	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥)
118	115, 117	eqssd 3925	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
119	81, 118	syldan 603	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
120	75, 119	sylan2 605	. . . . . . . . . 10 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
121	120	fveq2d 6889	. . . . . . . . 9 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
122	120	fveq2d 6889	. . . . . . . . 9 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
123	121, 122	breq12d 5115	. . . . . . . 8 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
124	123	biimpd 232	. . . . . . 7 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
125	124	ex 418	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
126	125	pm2.43d 54	. . . . 5 ⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
127	126	expimpd 459	. . . 4 ⊢ (𝑥 ∈ On → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
128	127	rexlimiv 3156	. . 3 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
129	50, 128	impbid1 228	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
130	1, 129	bitr4d 285	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ w3o 1102   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  {ctp 4588  ⟨cop 4834  ∩ cint 4906   class class class wbr 5102  Oncon0 6362  suc csuc 6364  ‘cfv 6538  1_oc1o 8472  2_oc2o 8473  Nocsur 28002   <s clts 28003

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-suc 6368  df-iota 6494  df-fv 6546  df-1o 8479  df-2o 8480  df-lts 28006

This theorem is used by:  ltsintdifex  28023  ltsres  28024  noextendlt  28031  noextendgt  28032  nosepnelem  28041  nosep1o  28043  nosep2o  28044  nosepdmlem  28045  nodenselem8  28053  nosupbnd2lem1  28077  noinfbnd2lem1  28092