soseq

Description: A linear ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011)

	Ref	Expression
Hypotheses	soseq.1	$⊢ R Or (A \cup \{\emptyset\})$
	soseq.2	$⊢ F = \{f \| \exists x \in On f : x ⟶ A\}$
	soseq.3	$⊢ S = \{⟨f, g⟩ \| ((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)))\}$
	soseq.4	$⊢ \neg \emptyset \in A$
Assertion	soseq	$⊢ S Or F$

Proof

Step	Hyp	Ref	Expression
1		soseq.1	$⊢ R Or (A \cup \{\emptyset\})$
2		soseq.2	$⊢ F = \{f \| \exists x \in On f : x ⟶ A\}$
3		soseq.3	$⊢ S = \{⟨f, g⟩ \| ((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)))\}$
4		soseq.4	$⊢ \neg \emptyset \in A$
5		sopo	$⊢ R Or (A \cup \{\emptyset\}) \to R Po (A \cup \{\emptyset\})$
6	1 5	ax-mp	$⊢ R Po (A \cup \{\emptyset\})$
7	6 2 3	poseq	$⊢ S Po F$
8		eleq1w	$⊢ f = a \to (f \in F \leftrightarrow a \in F)$
9	8	anbi1d	$⊢ f = a \to ((f \in F \land g \in F) \leftrightarrow (a \in F \land g \in F))$
10		fveq1	$⊢ f = a \to f (y) = a (y)$
11	10	eqeq1d	$⊢ f = a \to (f (y) = g (y) \leftrightarrow a (y) = g (y))$
12	11	ralbidv	$⊢ f = a \to (\forall y \in x f (y) = g (y) \leftrightarrow \forall y \in x a (y) = g (y))$
13		fveq1	$⊢ f = a \to f (x) = a (x)$
14	13	breq1d	$⊢ f = a \to (f (x) R g (x) \leftrightarrow a (x) R g (x))$
15	12 14	anbi12d	$⊢ f = a \to ((\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow (\forall y \in x a (y) = g (y) \land a (x) R g (x)))$
16	15	rexbidv	$⊢ f = a \to (\exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x)))$
17	9 16	anbi12d	$⊢ f = a \to (((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x))) \leftrightarrow ((a \in F \land g \in F) \land \exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x))))$
18		eleq1w	$⊢ g = b \to (g \in F \leftrightarrow b \in F)$
19	18	anbi2d	$⊢ g = b \to ((a \in F \land g \in F) \leftrightarrow (a \in F \land b \in F))$
20		fveq1	$⊢ g = b \to g (y) = b (y)$
21	20	eqeq2d	$⊢ g = b \to (a (y) = g (y) \leftrightarrow a (y) = b (y))$
22	21	ralbidv	$⊢ g = b \to (\forall y \in x a (y) = g (y) \leftrightarrow \forall y \in x a (y) = b (y))$
23		fveq1	$⊢ g = b \to g (x) = b (x)$
24	23	breq2d	$⊢ g = b \to (a (x) R g (x) \leftrightarrow a (x) R b (x))$
25	22 24	anbi12d	$⊢ g = b \to ((\forall y \in x a (y) = g (y) \land a (x) R g (x)) \leftrightarrow (\forall y \in x a (y) = b (y) \land a (x) R b (x)))$
26	25	rexbidv	$⊢ g = b \to (\exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x)) \leftrightarrow \exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)))$
27	19 26	anbi12d	$⊢ g = b \to (((a \in F \land g \in F) \land \exists x \in On (\forall y \in x a (y) = g (y) \land a (x) R g (x))) \leftrightarrow ((a \in F \land b \in F) \land \exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x))))$
28	17 27 3	brabg	$⊢ (a \in F \land b \in F) \to (a S b \leftrightarrow ((a \in F \land b \in F) \land \exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x))))$
29	28	bianabs	$⊢ (a \in F \land b \in F) \to (a S b \leftrightarrow \exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)))$
30		eleq1w	$⊢ f = b \to (f \in F \leftrightarrow b \in F)$
31	30	anbi1d	$⊢ f = b \to ((f \in F \land g \in F) \leftrightarrow (b \in F \land g \in F))$
32		fveq1	$⊢ f = b \to f (y) = b (y)$
33	32	eqeq1d	$⊢ f = b \to (f (y) = g (y) \leftrightarrow b (y) = g (y))$
34	33	ralbidv	$⊢ f = b \to (\forall y \in x f (y) = g (y) \leftrightarrow \forall y \in x b (y) = g (y))$
35		fveq1	$⊢ f = b \to f (x) = b (x)$
36	35	breq1d	$⊢ f = b \to (f (x) R g (x) \leftrightarrow b (x) R g (x))$
37	34 36	anbi12d	$⊢ f = b \to ((\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow (\forall y \in x b (y) = g (y) \land b (x) R g (x)))$
38	37	rexbidv	$⊢ f = b \to (\exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x)) \leftrightarrow \exists x \in On (\forall y \in x b (y) = g (y) \land b (x) R g (x)))$
39	31 38	anbi12d	$⊢ f = b \to (((f \in F \land g \in F) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) R g (x))) \leftrightarrow ((b \in F \land g \in F) \land \exists x \in On (\forall y \in x b (y) = g (y) \land b (x) R g (x))))$
40		eleq1w	$⊢ g = a \to (g \in F \leftrightarrow a \in F)$
41	40	anbi2d	$⊢ g = a \to ((b \in F \land g \in F) \leftrightarrow (b \in F \land a \in F))$
42		fveq1	$⊢ g = a \to g (y) = a (y)$
43	42	eqeq2d	$⊢ g = a \to (b (y) = g (y) \leftrightarrow b (y) = a (y))$
44	43	ralbidv	$⊢ g = a \to (\forall y \in x b (y) = g (y) \leftrightarrow \forall y \in x b (y) = a (y))$
45		fveq1	$⊢ g = a \to g (x) = a (x)$
46	45	breq2d	$⊢ g = a \to (b (x) R g (x) \leftrightarrow b (x) R a (x))$
47	44 46	anbi12d	$⊢ g = a \to ((\forall y \in x b (y) = g (y) \land b (x) R g (x)) \leftrightarrow (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
48	47	rexbidv	$⊢ g = a \to (\exists x \in On (\forall y \in x b (y) = g (y) \land b (x) R g (x)) \leftrightarrow \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
49	41 48	anbi12d	$⊢ g = a \to (((b \in F \land g \in F) \land \exists x \in On (\forall y \in x b (y) = g (y) \land b (x) R g (x))) \leftrightarrow ((b \in F \land a \in F) \land \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x))))$
50	39 49 3	brabg	$⊢ (b \in F \land a \in F) \to (b S a \leftrightarrow ((b \in F \land a \in F) \land \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x))))$
51	50	bianabs	$⊢ (b \in F \land a \in F) \to (b S a \leftrightarrow \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
52	51	ancoms	$⊢ (a \in F \land b \in F) \to (b S a \leftrightarrow \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
53	29 52	orbi12d	$⊢ (a \in F \land b \in F) \to ((a S b \lor b S a) \leftrightarrow (\exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x))))$
54	53	notbid	$⊢ (a \in F \land b \in F) \to (\neg (a S b \lor b S a) \leftrightarrow \neg (\exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x))))$
55		ralinexa	$⊢ \forall x \in On (\forall y \in x a (y) = b (y) \to \neg (a (x) R b (x) \lor b (x) R a (x))) \leftrightarrow \neg \exists x \in On (\forall y \in x a (y) = b (y) \land (a (x) R b (x) \lor b (x) R a (x)))$
56		andi	$⊢ (\forall y \in x a (y) = b (y) \land (a (x) R b (x) \lor b (x) R a (x))) \leftrightarrow ((\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor (\forall y \in x a (y) = b (y) \land b (x) R a (x)))$
57		eqcom	$⊢ a (y) = b (y) \leftrightarrow b (y) = a (y)$
58	57	ralbii	$⊢ \forall y \in x a (y) = b (y) \leftrightarrow \forall y \in x b (y) = a (y)$
59	58	anbi1i	$⊢ (\forall y \in x a (y) = b (y) \land b (x) R a (x)) \leftrightarrow (\forall y \in x b (y) = a (y) \land b (x) R a (x))$
60	59	orbi2i	$⊢ ((\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor (\forall y \in x a (y) = b (y) \land b (x) R a (x))) \leftrightarrow ((\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
61	56 60	bitri	$⊢ (\forall y \in x a (y) = b (y) \land (a (x) R b (x) \lor b (x) R a (x))) \leftrightarrow ((\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
62	61	rexbii	$⊢ \exists x \in On (\forall y \in x a (y) = b (y) \land (a (x) R b (x) \lor b (x) R a (x))) \leftrightarrow \exists x \in On ((\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
63		r19.43	$⊢ \exists x \in On ((\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor (\forall y \in x b (y) = a (y) \land b (x) R a (x))) \leftrightarrow (\exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
64	62 63	bitri	$⊢ \exists x \in On (\forall y \in x a (y) = b (y) \land (a (x) R b (x) \lor b (x) R a (x))) \leftrightarrow (\exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
65	55 64	xchbinx	$⊢ \forall x \in On (\forall y \in x a (y) = b (y) \to \neg (a (x) R b (x) \lor b (x) R a (x))) \leftrightarrow \neg (\exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x)))$
66		feq2	$⊢ x = y \to (f : x ⟶ A \leftrightarrow f : y ⟶ A)$
67	66	cbvrexvw	$⊢ \exists x \in On f : x ⟶ A \leftrightarrow \exists y \in On f : y ⟶ A$
68	67	abbii	$⊢ \{f \| \exists x \in On f : x ⟶ A\} = \{f \| \exists y \in On f : y ⟶ A\}$
69	2 68	eqtri	$⊢ F = \{f \| \exists y \in On f : y ⟶ A\}$
70	69	orderseqlem	$⊢ a \in F \to a (x) \in (A \cup \{\emptyset\})$
71	69	orderseqlem	$⊢ b \in F \to b (x) \in (A \cup \{\emptyset\})$
72		sotrieq	$⊢ (R Or (A \cup \{\emptyset\}) \land (a (x) \in (A \cup \{\emptyset\}) \land b (x) \in (A \cup \{\emptyset\}))) \to (a (x) = b (x) \leftrightarrow \neg (a (x) R b (x) \lor b (x) R a (x)))$
73	1 72	mpan	$⊢ (a (x) \in (A \cup \{\emptyset\}) \land b (x) \in (A \cup \{\emptyset\})) \to (a (x) = b (x) \leftrightarrow \neg (a (x) R b (x) \lor b (x) R a (x)))$
74	70 71 73	syl2an	$⊢ (a \in F \land b \in F) \to (a (x) = b (x) \leftrightarrow \neg (a (x) R b (x) \lor b (x) R a (x)))$
75	74	imbi2d	$⊢ (a \in F \land b \in F) \to ((\forall y \in x a (y) = b (y) \to a (x) = b (x)) \leftrightarrow (\forall y \in x a (y) = b (y) \to \neg (a (x) R b (x) \lor b (x) R a (x))))$
76	75	ralbidv	$⊢ (a \in F \land b \in F) \to (\forall x \in On (\forall y \in x a (y) = b (y) \to a (x) = b (x)) \leftrightarrow \forall x \in On (\forall y \in x a (y) = b (y) \to \neg (a (x) R b (x) \lor b (x) R a (x))))$
77		vex	$⊢ y \in V$
78		fveq2	$⊢ x = y \to a (x) = a (y)$
79		fveq2	$⊢ x = y \to b (x) = b (y)$
80	78 79	eqeq12d	$⊢ x = y \to (a (x) = b (x) \leftrightarrow a (y) = b (y))$
81	77 80	sbcie	$⊢ \underset{˙}{[} y / x \underset{˙}{]} a (x) = b (x) \leftrightarrow a (y) = b (y)$
82	81	ralbii	$⊢ \forall y \in x \underset{˙}{[} y / x \underset{˙}{]} a (x) = b (x) \leftrightarrow \forall y \in x a (y) = b (y)$
83	82	imbi1i	$⊢ (\forall y \in x \underset{˙}{[} y / x \underset{˙}{]} a (x) = b (x) \to a (x) = b (x)) \leftrightarrow (\forall y \in x a (y) = b (y) \to a (x) = b (x))$
84	83	ralbii	$⊢ \forall x \in On (\forall y \in x \underset{˙}{[} y / x \underset{˙}{]} a (x) = b (x) \to a (x) = b (x)) \leftrightarrow \forall x \in On (\forall y \in x a (y) = b (y) \to a (x) = b (x))$
85		tfisg	$⊢ \forall x \in On (\forall y \in x \underset{˙}{[} y / x \underset{˙}{]} a (x) = b (x) \to a (x) = b (x)) \to \forall x \in On a (x) = b (x)$
86	84 85	sylbir	$⊢ \forall x \in On (\forall y \in x a (y) = b (y) \to a (x) = b (x)) \to \forall x \in On a (x) = b (x)$
87		vex	$⊢ a \in V$
88		feq1	$⊢ f = a \to (f : x ⟶ A \leftrightarrow a : x ⟶ A)$
89	88	rexbidv	$⊢ f = a \to (\exists x \in On f : x ⟶ A \leftrightarrow \exists x \in On a : x ⟶ A)$
90	87 89 2	elab2	$⊢ a \in F \leftrightarrow \exists x \in On a : x ⟶ A$
91		feq2	$⊢ x = p \to (a : x ⟶ A \leftrightarrow a : p ⟶ A)$
92	91	cbvrexvw	$⊢ \exists x \in On a : x ⟶ A \leftrightarrow \exists p \in On a : p ⟶ A$
93	90 92	bitri	$⊢ a \in F \leftrightarrow \exists p \in On a : p ⟶ A$
94		vex	$⊢ b \in V$
95		feq1	$⊢ f = b \to (f : x ⟶ A \leftrightarrow b : x ⟶ A)$
96	95	rexbidv	$⊢ f = b \to (\exists x \in On f : x ⟶ A \leftrightarrow \exists x \in On b : x ⟶ A)$
97	94 96 2	elab2	$⊢ b \in F \leftrightarrow \exists x \in On b : x ⟶ A$
98		feq2	$⊢ x = q \to (b : x ⟶ A \leftrightarrow b : q ⟶ A)$
99	98	cbvrexvw	$⊢ \exists x \in On b : x ⟶ A \leftrightarrow \exists q \in On b : q ⟶ A$
100	97 99	bitri	$⊢ b \in F \leftrightarrow \exists q \in On b : q ⟶ A$
101	93 100	anbi12i	$⊢ (a \in F \land b \in F) \leftrightarrow (\exists p \in On a : p ⟶ A \land \exists q \in On b : q ⟶ A)$
102		reeanv	$⊢ \exists p \in On \exists q \in On (a : p ⟶ A \land b : q ⟶ A) \leftrightarrow (\exists p \in On a : p ⟶ A \land \exists q \in On b : q ⟶ A)$
103	101 102	bitr4i	$⊢ (a \in F \land b \in F) \leftrightarrow \exists p \in On \exists q \in On (a : p ⟶ A \land b : q ⟶ A)$
104		onss	$⊢ q \in On \to q \subseteq On$
105		ssralv	$⊢ q \subseteq On \to (\forall x \in On a (x) = b (x) \to \forall x \in q a (x) = b (x))$
106	104 105	syl	$⊢ q \in On \to (\forall x \in On a (x) = b (x) \to \forall x \in q a (x) = b (x))$
107	106	ad2antlr	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to \forall x \in q a (x) = b (x))$
108		fveq2	$⊢ x = p \to a (x) = a (p)$
109		fveq2	$⊢ x = p \to b (x) = b (p)$
110	108 109	eqeq12d	$⊢ x = p \to (a (x) = b (x) \leftrightarrow a (p) = b (p))$
111	110	rspcv	$⊢ p \in q \to (\forall x \in q a (x) = b (x) \to a (p) = b (p))$
112	111	a1i	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (p \in q \to (\forall x \in q a (x) = b (x) \to a (p) = b (p)))$
113		ffvelrn	$⊢ (b : q ⟶ A \land p \in q) \to b (p) \in A$
114		fdm	$⊢ a : p ⟶ A \to dom a = p$
115		eloni	$⊢ p \in On \to Ord p$
116		ordirr	$⊢ Ord p \to \neg p \in p$
117	115 116	syl	$⊢ p \in On \to \neg p \in p$
118		eleq2	$⊢ dom a = p \to (p \in dom a \leftrightarrow p \in p)$
119	118	notbid	$⊢ dom a = p \to (\neg p \in dom a \leftrightarrow \neg p \in p)$
120	119	biimparc	$⊢ (\neg p \in p \land dom a = p) \to \neg p \in dom a$
121	117 120	sylan	$⊢ (p \in On \land dom a = p) \to \neg p \in dom a$
122		ndmfv	$⊢ \neg p \in dom a \to a (p) = \emptyset$
123		eqtr2	$⊢ (a (p) = \emptyset \land a (p) = b (p)) \to \emptyset = b (p)$
124		eleq1	$⊢ \emptyset = b (p) \to (\emptyset \in A \leftrightarrow b (p) \in A)$
125	124	biimprd	$⊢ \emptyset = b (p) \to (b (p) \in A \to \emptyset \in A)$
126	123 125	syl	$⊢ (a (p) = \emptyset \land a (p) = b (p)) \to (b (p) \in A \to \emptyset \in A)$
127	126	ex	$⊢ a (p) = \emptyset \to (a (p) = b (p) \to (b (p) \in A \to \emptyset \in A))$
128	121 122 127	3syl	$⊢ (p \in On \land dom a = p) \to (a (p) = b (p) \to (b (p) \in A \to \emptyset \in A))$
129	128	com23	$⊢ (p \in On \land dom a = p) \to (b (p) \in A \to (a (p) = b (p) \to \emptyset \in A))$
130	114 129	sylan2	$⊢ (p \in On \land a : p ⟶ A) \to (b (p) \in A \to (a (p) = b (p) \to \emptyset \in A))$
131	130	adantlr	$⊢ ((p \in On \land q \in On) \land a : p ⟶ A) \to (b (p) \in A \to (a (p) = b (p) \to \emptyset \in A))$
132	113 131	syl5	$⊢ ((p \in On \land q \in On) \land a : p ⟶ A) \to ((b : q ⟶ A \land p \in q) \to (a (p) = b (p) \to \emptyset \in A))$
133	132	exp4b	$⊢ (p \in On \land q \in On) \to (a : p ⟶ A \to (b : q ⟶ A \to (p \in q \to (a (p) = b (p) \to \emptyset \in A))))$
134	133	imp32	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (p \in q \to (a (p) = b (p) \to \emptyset \in A))$
135	112 134	syldd	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (p \in q \to (\forall x \in q a (x) = b (x) \to \emptyset \in A))$
136	135	com23	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in q a (x) = b (x) \to (p \in q \to \emptyset \in A))$
137	136	imp	$⊢ (((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \land \forall x \in q a (x) = b (x)) \to (p \in q \to \emptyset \in A)$
138	4 137	mtoi	$⊢ (((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \land \forall x \in q a (x) = b (x)) \to \neg p \in q$
139	138	ex	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in q a (x) = b (x) \to \neg p \in q)$
140	107 139	syld	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to \neg p \in q)$
141		onss	$⊢ p \in On \to p \subseteq On$
142		ssralv	$⊢ p \subseteq On \to (\forall x \in On a (x) = b (x) \to \forall x \in p a (x) = b (x))$
143	141 142	syl	$⊢ p \in On \to (\forall x \in On a (x) = b (x) \to \forall x \in p a (x) = b (x))$
144	143	ad2antrr	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to \forall x \in p a (x) = b (x))$
145		fveq2	$⊢ x = q \to a (x) = a (q)$
146		fveq2	$⊢ x = q \to b (x) = b (q)$
147	145 146	eqeq12d	$⊢ x = q \to (a (x) = b (x) \leftrightarrow a (q) = b (q))$
148	147	rspcv	$⊢ q \in p \to (\forall x \in p a (x) = b (x) \to a (q) = b (q))$
149	148	a1i	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (q \in p \to (\forall x \in p a (x) = b (x) \to a (q) = b (q)))$
150		ffvelrn	$⊢ (a : p ⟶ A \land q \in p) \to a (q) \in A$
151		fdm	$⊢ b : q ⟶ A \to dom b = q$
152		eloni	$⊢ q \in On \to Ord q$
153		ordirr	$⊢ Ord q \to \neg q \in q$
154	152 153	syl	$⊢ q \in On \to \neg q \in q$
155		eleq2	$⊢ dom b = q \to (q \in dom b \leftrightarrow q \in q)$
156	155	notbid	$⊢ dom b = q \to (\neg q \in dom b \leftrightarrow \neg q \in q)$
157	156	biimparc	$⊢ (\neg q \in q \land dom b = q) \to \neg q \in dom b$
158		ndmfv	$⊢ \neg q \in dom b \to b (q) = \emptyset$
159	157 158	syl	$⊢ (\neg q \in q \land dom b = q) \to b (q) = \emptyset$
160	154 159	sylan	$⊢ (q \in On \land dom b = q) \to b (q) = \emptyset$
161		eqtr	$⊢ (a (q) = b (q) \land b (q) = \emptyset) \to a (q) = \emptyset$
162		eleq1	$⊢ a (q) = \emptyset \to (a (q) \in A \leftrightarrow \emptyset \in A)$
163	162	biimpd	$⊢ a (q) = \emptyset \to (a (q) \in A \to \emptyset \in A)$
164	161 163	syl	$⊢ (a (q) = b (q) \land b (q) = \emptyset) \to (a (q) \in A \to \emptyset \in A)$
165	164	expcom	$⊢ b (q) = \emptyset \to (a (q) = b (q) \to (a (q) \in A \to \emptyset \in A))$
166	165	com23	$⊢ b (q) = \emptyset \to (a (q) \in A \to (a (q) = b (q) \to \emptyset \in A))$
167	160 166	syl	$⊢ (q \in On \land dom b = q) \to (a (q) \in A \to (a (q) = b (q) \to \emptyset \in A))$
168	167	adantll	$⊢ ((p \in On \land q \in On) \land dom b = q) \to (a (q) \in A \to (a (q) = b (q) \to \emptyset \in A))$
169	151 168	sylan2	$⊢ ((p \in On \land q \in On) \land b : q ⟶ A) \to (a (q) \in A \to (a (q) = b (q) \to \emptyset \in A))$
170	150 169	syl5	$⊢ ((p \in On \land q \in On) \land b : q ⟶ A) \to ((a : p ⟶ A \land q \in p) \to (a (q) = b (q) \to \emptyset \in A))$
171	170	exp4b	$⊢ (p \in On \land q \in On) \to (b : q ⟶ A \to (a : p ⟶ A \to (q \in p \to (a (q) = b (q) \to \emptyset \in A))))$
172	171	com23	$⊢ (p \in On \land q \in On) \to (a : p ⟶ A \to (b : q ⟶ A \to (q \in p \to (a (q) = b (q) \to \emptyset \in A))))$
173	172	imp32	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (q \in p \to (a (q) = b (q) \to \emptyset \in A))$
174	149 173	syldd	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (q \in p \to (\forall x \in p a (x) = b (x) \to \emptyset \in A))$
175	174	com23	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in p a (x) = b (x) \to (q \in p \to \emptyset \in A))$
176	175	imp	$⊢ (((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \land \forall x \in p a (x) = b (x)) \to (q \in p \to \emptyset \in A)$
177	4 176	mtoi	$⊢ (((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \land \forall x \in p a (x) = b (x)) \to \neg q \in p$
178	177	ex	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in p a (x) = b (x) \to \neg q \in p)$
179	144 178	syld	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to \neg q \in p)$
180	140 179	jcad	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to (\neg p \in q \land \neg q \in p))$
181		ordtri3or	$⊢ (Ord p \land Ord q) \to (p \in q \lor p = q \lor q \in p)$
182	115 152 181	syl2an	$⊢ (p \in On \land q \in On) \to (p \in q \lor p = q \lor q \in p)$
183	182	adantr	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (p \in q \lor p = q \lor q \in p)$
184		3orel13	$⊢ (\neg p \in q \land \neg q \in p) \to ((p \in q \lor p = q \lor q \in p) \to p = q)$
185	180 183 184	syl6ci	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to p = q)$
186	185 144	jcad	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to (p = q \land \forall x \in p a (x) = b (x)))$
187		ffn	$⊢ a : p ⟶ A \to a Fn p$
188		ffn	$⊢ b : q ⟶ A \to b Fn q$
189		eqfnfv2	$⊢ (a Fn p \land b Fn q) \to (a = b \leftrightarrow (p = q \land \forall x \in p a (x) = b (x)))$
190	187 188 189	syl2an	$⊢ (a : p ⟶ A \land b : q ⟶ A) \to (a = b \leftrightarrow (p = q \land \forall x \in p a (x) = b (x)))$
191	190	adantl	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (a = b \leftrightarrow (p = q \land \forall x \in p a (x) = b (x)))$
192	186 191	sylibrd	$⊢ ((p \in On \land q \in On) \land (a : p ⟶ A \land b : q ⟶ A)) \to (\forall x \in On a (x) = b (x) \to a = b)$
193	192	ex	$⊢ (p \in On \land q \in On) \to ((a : p ⟶ A \land b : q ⟶ A) \to (\forall x \in On a (x) = b (x) \to a = b))$
194	193	rexlimivv	$⊢ \exists p \in On \exists q \in On (a : p ⟶ A \land b : q ⟶ A) \to (\forall x \in On a (x) = b (x) \to a = b)$
195	103 194	sylbi	$⊢ (a \in F \land b \in F) \to (\forall x \in On a (x) = b (x) \to a = b)$
196	86 195	syl5	$⊢ (a \in F \land b \in F) \to (\forall x \in On (\forall y \in x a (y) = b (y) \to a (x) = b (x)) \to a = b)$
197	76 196	sylbird	$⊢ (a \in F \land b \in F) \to (\forall x \in On (\forall y \in x a (y) = b (y) \to \neg (a (x) R b (x) \lor b (x) R a (x))) \to a = b)$
198	65 197	syl5bir	$⊢ (a \in F \land b \in F) \to (\neg (\exists x \in On (\forall y \in x a (y) = b (y) \land a (x) R b (x)) \lor \exists x \in On (\forall y \in x b (y) = a (y) \land b (x) R a (x))) \to a = b)$
199	54 198	sylbid	$⊢ (a \in F \land b \in F) \to (\neg (a S b \lor b S a) \to a = b)$
200	199	orrd	$⊢ (a \in F \land b \in F) \to ((a S b \lor b S a) \lor a = b)$
201		3orcomb	$⊢ (a S b \lor a = b \lor b S a) \leftrightarrow (a S b \lor b S a \lor a = b)$
202		df-3or	$⊢ (a S b \lor b S a \lor a = b) \leftrightarrow ((a S b \lor b S a) \lor a = b)$
203	201 202	bitr2i	$⊢ ((a S b \lor b S a) \lor a = b) \leftrightarrow (a S b \lor a = b \lor b S a)$
204	200 203	sylib	$⊢ (a \in F \land b \in F) \to (a S b \lor a = b \lor b S a)$
205	204	rgen2	$⊢ \forall a \in F \forall b \in F (a S b \lor a = b \lor b S a)$
206		df-so	$⊢ S Or F \leftrightarrow (S Po F \land \forall a \in F \forall b \in F (a S b \lor a = b \lor b S a))$
207	7 205 206	mpbir2an	$⊢ S Or F$

Metamath Proof Explorer

Theorem soseq

Proof