Theorem sltval2 31053

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
sltval2	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))

Distinct variable groups:   𝐴,𝑎   𝐵,𝑎

Proof of Theorem sltval2

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

Step	Hyp	Ref	Expression
1		sltval 31044	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥))))
2		fvex 6113	. . . . . . . . . . . . 13 ⊢ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V
3		fvex 6113	. . . . . . . . . . . . 13 ⊢ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V
4	2, 3	brtp 30892	. . . . . . . . . . . 12 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜)))
5		1n0 7462	. . . . . . . . . . . . . . . . 17 ⊢ 1𝑜 ≠ ∅
6	5	neii 2784	. . . . . . . . . . . . . . . 16 ⊢ ¬ 1𝑜 = ∅
7		eqeq1 2614	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ↔ 1𝑜 = ∅))
8	6, 7	mtbiri 316	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
9		fvprc 6097	. . . . . . . . . . . . . . 15 ⊢ (¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
10	8, 9	nsyl2 141	. . . . . . . . . . . . . 14 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
11	10	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
12	10	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
13		2on0 7456	. . . . . . . . . . . . . . . . 17 ⊢ 2𝑜 ≠ ∅
14	13	neii 2784	. . . . . . . . . . . . . . . 16 ⊢ ¬ 2𝑜 = ∅
15		eqeq1 2614	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜 → ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ↔ 2𝑜 = ∅))
16	14, 15	mtbiri 316	. . . . . . . . . . . . . . 15 ⊢ ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜 → ¬ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
17		fvprc 6097	. . . . . . . . . . . . . . 15 ⊢ (¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅)
18	16, 17	nsyl2 141	. . . . . . . . . . . . . 14 ⊢ ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
19	18	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
20	11, 12, 19	3jaoi 1383	. . . . . . . . . . . 12 ⊢ ((((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
21	4, 20	sylbi 206	. . . . . . . . . . 11 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)
22		onintrab 6893	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V ↔ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
23	21, 22	sylib 207	. . . . . . . . . 10 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
24	23	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
25		onelon 5665	. . . . . . . . . . . . . . 15 ⊢ ((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑦 ∈ On)
26	25	expcom 450	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On → 𝑦 ∈ On))
27	24, 26	syl5 33	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → 𝑦 ∈ On))
28		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑦 → (𝐴‘𝑎) = (𝐴‘𝑦))
29		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑦 → (𝐵‘𝑎) = (𝐵‘𝑦))
30	28, 29	neeq12d 2843	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑦 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
31	30	onnminsb 6896	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ On → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
32	31	com12 32	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝑦 ∈ On → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
33	27, 32	syld 46	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
34	33	com12 32	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)))
35		df-ne 2782	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑦) ≠ (𝐵‘𝑦) ↔ ¬ (𝐴‘𝑦) = (𝐵‘𝑦))
36	35	con2bii 346	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦))
37	34, 36	syl6ibr 241	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = (𝐵‘𝑦)))
38	37	ralrimiv 2948	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))
39	24, 38	jca 553	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
40	39	ex 449	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))))
41	40	impac 649	. . . . . 6 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
42		anass 679	. . . . . 6 ⊢ (((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) ↔ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
43	41, 42	sylib 207	. . . . 5 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
44		raleq 3115	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
45		fveq2 6103	. . . . . . . 8 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
46		fveq2 6103	. . . . . . . 8 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
47	45, 46	breq12d 4596	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
48	44, 47	anbi12d 743	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
49	48	rspcev 3282	. . . . 5 ⊢ ((∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)))
50	43, 49	syl 17	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)))
51	50	ex 449	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥))))
52		eqeq12 2623	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = ∅) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 1𝑜 = ∅))
53	6, 52	mtbiri 316	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = ∅) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
54		1on 7454	. . . . . . . . . . . . . . . . 17 ⊢ 1𝑜 ∈ On
55		0elon 5695	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ On
56		suc11 5748	. . . . . . . . . . . . . . . . . 18 ⊢ ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 = suc ∅ ↔ 1𝑜 = ∅))
57	56	necon3bid 2826	. . . . . . . . . . . . . . . . 17 ⊢ ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅))
58	54, 55, 57	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅)
59	5, 58	mpbir 220	. . . . . . . . . . . . . . 15 ⊢ suc 1𝑜 ≠ suc ∅
60		df-2o 7448	. . . . . . . . . . . . . . . 16 ⊢ 2𝑜 = suc 1𝑜
61		df-1o 7447	. . . . . . . . . . . . . . . 16 ⊢ 1𝑜 = suc ∅
62	60, 61	eqeq12i 2624	. . . . . . . . . . . . . . 15 ⊢ (2𝑜 = 1𝑜 ↔ suc 1𝑜 = suc ∅)
63	59, 62	nemtbir 2877	. . . . . . . . . . . . . 14 ⊢ ¬ 2𝑜 = 1𝑜
64		eqeq12 2623	. . . . . . . . . . . . . . 15 ⊢ (((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = 2𝑜) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 1𝑜 = 2𝑜))
65		eqcom 2617	. . . . . . . . . . . . . . 15 ⊢ (1𝑜 = 2𝑜 ↔ 2𝑜 = 1𝑜)
66	64, 65	syl6bb 275	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = 2𝑜) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 2𝑜 = 1𝑜))
67	63, 66	mtbiri 316	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = 2𝑜) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
68	13	nesymi 2839	. . . . . . . . . . . . . 14 ⊢ ¬ ∅ = 2𝑜
69		eqeq12 2623	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2𝑜) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ ∅ = 2𝑜))
70	68, 69	mtbiri 316	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2𝑜) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
71	53, 67, 70	3jaoi 1383	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = ∅) ∨ ((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = 2𝑜) ∨ ((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2𝑜)) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
72		fvex 6113	. . . . . . . . . . . . 13 ⊢ (𝐴‘𝑥) ∈ V
73		fvex 6113	. . . . . . . . . . . . 13 ⊢ (𝐵‘𝑥) ∈ V
74	72, 73	brtp 30892	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) ↔ (((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = ∅) ∨ ((𝐴‘𝑥) = 1𝑜 ∧ (𝐵‘𝑥) = 2𝑜) ∨ ((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2𝑜)))
75		df-ne 2782	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑥) = (𝐵‘𝑥))
76	71, 74, 75	3imtr4i 280	. . . . . . . . . . 11 ⊢ ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) → (𝐴‘𝑥) ≠ (𝐵‘𝑥))
77		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝐴‘𝑎) = (𝐴‘𝑥))
78		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝐵‘𝑎) = (𝐵‘𝑥))
79	77, 78	neeq12d 2843	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝑥) ≠ (𝐵‘𝑥)))
80	79	elrab 3331	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)))
81	80	biimpri 217	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
82	81	adantlr 747	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
83		ssrab2 3650	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On
84		ne0i 3880	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅)
85	84	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅)
86		onint 6887	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
87	83, 85, 86	sylancr 694	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
88		nfrab1 3099	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}
89	88	nfint 4421	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}
90		nfcv 2751	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎On
91		nfcv 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎𝐴
92	91, 89	nffv 6110	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎(𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
93		nfcv 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎𝐵
94	93, 89	nffv 6110	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎(𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
95	92, 94	nfne 2882	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎(𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
96		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑎) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
97		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑎) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
98	96, 97	neeq12d 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
99	89, 90, 95, 98	elrabf 3329	. . . . . . . . . . . . . . . . . 18 ⊢ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
100	99	simprbi 479	. . . . . . . . . . . . . . . . 17 ⊢ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
101	87, 100	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
102		df-ne 2782	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
103	101, 102	sylib 207	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
104		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
105		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑦) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
106	104, 105	eqeq12d 2625	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
107	106	rspccv 3279	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥 → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
108	107	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥 → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
109	103, 108	mtod 188	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥)
110		simpll 786	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 ∈ On)
111		oninton 6892	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
112	83, 84, 111	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
113	112	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
114		ontri1 5674	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) → (𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥))
115	110, 113, 114	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥))
116	109, 115	mpbird 246	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
117		intss1 4427	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥)
118	117	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥)
119	116, 118	eqssd 3585	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
120	82, 119	syldan 486	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
121	76, 120	sylan2 490	. . . . . . . . . 10 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})
122	121	fveq2d 6107	. . . . . . . . 9 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
123	121	fveq2d 6107	. . . . . . . . 9 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
124	122, 123	breq12d 4596	. . . . . . . 8 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) → ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
125	124	biimpd 218	. . . . . . 7 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) → ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
126	125	ex 449	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) → ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) → ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))))
127	126	pm2.43d 51	. . . . 5 ⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) → ((𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
128	127	expimpd 627	. . . 4 ⊢ (𝑥 ∈ On → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
129	128	rexlimiv 3009	. . 3 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))
130	51, 129	impbid1 214	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘𝑥))))
131	1, 130	bitr4d 270	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  {ctp 4129  ⟨cop 4131  ∩ cint 4410   class class class wbr 4583  Oncon0 5640  suc csuc 5642  ‘cfv 5804  1_𝑜c1o 7440  2_𝑜c2o 7441   No csur 31037   <s cslt 31038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644  df-suc 5646  df-iota 5768  df-fv 5812  df-1o 7447  df-2o 7448  df-slt 31041

This theorem is referenced by:  sltsgn1  31058  sltsgn2  31059  sltintdifex  31060  sltres  31061  nodenselem8  31087