Theorem sfinltfin 4536

Description: Ordering law for finite smaller than. Theorem X.1.47 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)

Assertion

Ref	Expression
sfinltfin	⊢ ((( Sfin (M, N) ∧ Sfin (P, Q)) ∧ ⟪M, P⟫ ∈ <fin ) → ⟪N, Q⟫ ∈ <fin )

Proof of Theorem sfinltfin

Dummy variables a b r s d g t x n u m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sfin 4447	. . 3 ⊢ ( Sfin (M, N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)))
2		df-sfin 4447	. . 3 ⊢ ( Sfin (P, Q) ↔ (P ∈ Nn ∧ Q ∈ Nn ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q)))
3		3an6 1262	. . . 4 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ (∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) ↔ ((M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)) ∧ (P ∈ Nn ∧ Q ∈ Nn ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))))
4		eeanv 1913	. . . . . 6 ⊢ (∃a∃b((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q)) ↔ (∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q)))
5		simp1l 979	. . . . . . . . . 10 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → M ∈ Nn )
6		simp3ll 1026	. . . . . . . . . 10 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ℘1a ∈ M)
7		ncfinlower 4484	. . . . . . . . . 10 ⊢ ((M ∈ Nn ∧ ℘1a ∈ M ∧ ℘1a ∈ M) → ∃r ∈ Nn (a ∈ r ∧ a ∈ r))
8	5, 6, 6, 7	syl3anc 1182	. . . . . . . . 9 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ∃r ∈ Nn (a ∈ r ∧ a ∈ r))
9		simp1r 980	. . . . . . . . . 10 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → P ∈ Nn )
10		simp3rl 1028	. . . . . . . . . 10 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ℘1b ∈ P)
11		ncfinlower 4484	. . . . . . . . . 10 ⊢ ((P ∈ Nn ∧ ℘1b ∈ P ∧ ℘1b ∈ P) → ∃s ∈ Nn (b ∈ s ∧ b ∈ s))
12	9, 10, 10, 11	syl3anc 1182	. . . . . . . . 9 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ∃s ∈ Nn (b ∈ s ∧ b ∈ s))
13		reeanv 2779	. . . . . . . . . 10 ⊢ (∃r ∈ Nn ∃s ∈ Nn ((a ∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) ↔ (∃r ∈ Nn (a ∈ r ∧ a ∈ r) ∧ ∃s ∈ Nn (b ∈ s ∧ b ∈ s)))
14		simpl 443	. . . . . . . . . . . . 13 ⊢ ((a ∈ r ∧ a ∈ r) → a ∈ r)
15		simpl 443	. . . . . . . . . . . . 13 ⊢ ((b ∈ s ∧ b ∈ s) → b ∈ s)
16	14, 15	anim12i 549	. . . . . . . . . . . 12 ⊢ (((a ∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) → (a ∈ r ∧ b ∈ s))
17	6	adantr 451	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ℘1a ∈ M)
18		simprll 738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → r ∈ Nn )
19		simprrl 740	. . . . . . . . . . . . . . . . . 18 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → a ∈ r)
20		tfinpw1 4495	. . . . . . . . . . . . . . . . . 18 ⊢ ((r ∈ Nn ∧ a ∈ r) → ℘1a ∈ Tfin r)
21	18, 19, 20	syl2anc 642	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ℘1a ∈ Tfin r)
22		elin 3220	. . . . . . . . . . . . . . . . 17 ⊢ (℘1a ∈ (M ∩ Tfin r) ↔ (℘1a ∈ M ∧ ℘1a ∈ Tfin r))
23	17, 21, 22	sylanbrc 645	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ℘1a ∈ (M ∩ Tfin r))
24		n0i 3556	. . . . . . . . . . . . . . . 16 ⊢ (℘1a ∈ (M ∩ Tfin r) → ¬ (M ∩ Tfin r) = ∅)
25	23, 24	syl 15	. . . . . . . . . . . . . . 15 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ¬ (M ∩ Tfin r) = ∅)
26		simpl1l 1006	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → M ∈ Nn )
27		ne0i 3557	. . . . . . . . . . . . . . . . . 18 ⊢ (a ∈ r → r ≠ ∅)
28	19, 27	syl 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → r ≠ ∅)
29		tfinprop 4490	. . . . . . . . . . . . . . . . . 18 ⊢ ((r ∈ Nn ∧ r ≠ ∅) → ( Tfin r ∈ Nn ∧ ∃a ∈ r ℘1a ∈ Tfin r))
30	29	simpld 445	. . . . . . . . . . . . . . . . 17 ⊢ ((r ∈ Nn ∧ r ≠ ∅) → Tfin r ∈ Nn )
31	18, 28, 30	syl2anc 642	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → Tfin r ∈ Nn )
32		nndisjeq 4430	. . . . . . . . . . . . . . . 16 ⊢ ((M ∈ Nn ∧ Tfin r ∈ Nn ) → ((M ∩ Tfin r) = ∅ ∨ M = Tfin r))
33	26, 31, 32	syl2anc 642	. . . . . . . . . . . . . . 15 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ((M ∩ Tfin r) = ∅ ∨ M = Tfin r))
34		orel1 371	. . . . . . . . . . . . . . 15 ⊢ (¬ (M ∩ Tfin r) = ∅ → (((M ∩ Tfin r) = ∅ ∨ M = Tfin r) → M = Tfin r))
35	25, 33, 34	sylc 56	. . . . . . . . . . . . . 14 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → M = Tfin r)
36	10	adantr 451	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ℘1b ∈ P)
37		simprlr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → s ∈ Nn )
38		simprrr 741	. . . . . . . . . . . . . . . . . 18 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → b ∈ s)
39		tfinpw1 4495	. . . . . . . . . . . . . . . . . 18 ⊢ ((s ∈ Nn ∧ b ∈ s) → ℘1b ∈ Tfin s)
40	37, 38, 39	syl2anc 642	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ℘1b ∈ Tfin s)
41		elin 3220	. . . . . . . . . . . . . . . . 17 ⊢ (℘1b ∈ (P ∩ Tfin s) ↔ (℘1b ∈ P ∧ ℘1b ∈ Tfin s))
42	36, 40, 41	sylanbrc 645	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ℘1b ∈ (P ∩ Tfin s))
43		n0i 3556	. . . . . . . . . . . . . . . 16 ⊢ (℘1b ∈ (P ∩ Tfin s) → ¬ (P ∩ Tfin s) = ∅)
44	42, 43	syl 15	. . . . . . . . . . . . . . 15 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ¬ (P ∩ Tfin s) = ∅)
45		simpl1r 1007	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → P ∈ Nn )
46		ne0i 3557	. . . . . . . . . . . . . . . . . 18 ⊢ (b ∈ s → s ≠ ∅)
47	38, 46	syl 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → s ≠ ∅)
48		tfinprop 4490	. . . . . . . . . . . . . . . . . 18 ⊢ ((s ∈ Nn ∧ s ≠ ∅) → ( Tfin s ∈ Nn ∧ ∃a ∈ s ℘1a ∈ Tfin s))
49	48	simpld 445	. . . . . . . . . . . . . . . . 17 ⊢ ((s ∈ Nn ∧ s ≠ ∅) → Tfin s ∈ Nn )
50	37, 47, 49	syl2anc 642	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → Tfin s ∈ Nn )
51		nndisjeq 4430	. . . . . . . . . . . . . . . 16 ⊢ ((P ∈ Nn ∧ Tfin s ∈ Nn ) → ((P ∩ Tfin s) = ∅ ∨ P = Tfin s))
52	45, 50, 51	syl2anc 642	. . . . . . . . . . . . . . 15 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ((P ∩ Tfin s) = ∅ ∨ P = Tfin s))
53		orel1 371	. . . . . . . . . . . . . . 15 ⊢ (¬ (P ∩ Tfin s) = ∅ → (((P ∩ Tfin s) = ∅ ∨ P = Tfin s) → P = Tfin s))
54	44, 52, 53	sylc 56	. . . . . . . . . . . . . 14 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → P = Tfin s)
55		tfinltfin 4502	. . . . . . . . . . . . . . . . 17 ⊢ ((r ∈ Nn ∧ s ∈ Nn ) → (⟪r, s⟫ ∈ <fin ↔ ⟪ Tfin r, Tfin s⟫ ∈ <fin ))
56	55	ad2antrl 708	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → (⟪r, s⟫ ∈ <fin ↔ ⟪ Tfin r, Tfin s⟫ ∈ <fin ))
57		opkltfing 4450	. . . . . . . . . . . . . . . . . 18 ⊢ ((r ∈ Nn ∧ s ∈ Nn ) → (⟪r, s⟫ ∈ <fin ↔ (r ≠ ∅ ∧ ∃t ∈ Nn s = ((r +c t) +c 1c))))
58	57	ad2antrl 708	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → (⟪r, s⟫ ∈ <fin ↔ (r ≠ ∅ ∧ ∃t ∈ Nn s = ((r +c t) +c 1c))))
59		simp2rr 1025	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → b ∈ s)
60		simp3r 984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → s = ((r +c t) +c 1c))
61	59, 60	eleqtrd 2429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → b ∈ ((r +c t) +c 1c))
62		addcass 4416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((r +c t) +c 1c) = (r +c (t +c 1c))
63	61, 62	syl6eleq 2443	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → b ∈ (r +c (t +c 1c)))
64		eladdc 4399	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (b ∈ (r +c (t +c 1c)) ↔ ∃g ∈ r ∃d ∈ (t +c 1c)((g ∩ d) = ∅ ∧ b = (g ∪ d)))
65		0nelsuc 4401	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ¬ ∅ ∈ (t +c 1c)
66		simprlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → d ∈ (t +c 1c))
67		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (d = ∅ → (d ∈ (t +c 1c) ↔ ∅ ∈ (t +c 1c)))
68	66, 67	syl5ibcom 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (d = ∅ → ∅ ∈ (t +c 1c)))
69	65, 68	mtoi 169	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → ¬ d = ∅)
70		df-ne 2519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (d ≠ ∅ ↔ ¬ d = ∅)
71	69, 70	sylibr 203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → d ≠ ∅)
72		n0 3560	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (d ≠ ∅ ↔ ∃x x ∈ d)
73		ssun2 3428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ d ⊆ (g ∪ d)
74		sseq2 3294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (b = (g ∪ d) → (d ⊆ b ↔ d ⊆ (g ∪ d)))
75	73, 74	mpbiri 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (b = (g ∪ d) → d ⊆ b)
76	75	sseld 3273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (b = (g ∪ d) → (x ∈ d → x ∈ b))
77		disjr 3593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((g ∩ d) = ∅ ↔ ∀x ∈ d ¬ x ∈ g)
78		rsp 2675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀x ∈ d ¬ x ∈ g → (x ∈ d → ¬ x ∈ g))
79	77, 78	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((g ∩ d) = ∅ → (x ∈ d → ¬ x ∈ g))
80	76, 79	anim12ii 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((b = (g ∪ d) ∧ (g ∩ d) = ∅) → (x ∈ d → (x ∈ b ∧ ¬ x ∈ g)))
81	80	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((g ∩ d) = ∅ ∧ b = (g ∪ d)) → (x ∈ d → (x ∈ b ∧ ¬ x ∈ g)))
82	81	ad2antll 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (x ∈ d → (x ∈ b ∧ ¬ x ∈ g)))
83		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ x ∈ V
84	83	snelpw 4116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({x} ∈ ℘b ↔ x ∈ b)
85	83	snelpw 4116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ({x} ∈ ℘g ↔ x ∈ g)
86	85	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (¬ {x} ∈ ℘g ↔ ¬ x ∈ g)
87	84, 86	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g) ↔ (x ∈ b ∧ ¬ x ∈ g))
88		ssun1 3427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ g ⊆ (g ∪ d)
89		sseq2 3294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (b = (g ∪ d) → (g ⊆ b ↔ g ⊆ (g ∪ d)))
90	88, 89	mpbiri 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (b = (g ∪ d) → g ⊆ b)
91		sspwb 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (g ⊆ b ↔ ℘g ⊆ ℘b)
92	90, 91	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (b = (g ∪ d) → ℘g ⊆ ℘b)
93	92	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((g ∩ d) = ∅ ∧ b = (g ∪ d)) → ℘g ⊆ ℘b)
94	93	ad2antll 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → ℘g ⊆ ℘b)
95		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (℘g = ℘b → ({x} ∈ ℘g ↔ {x} ∈ ℘b))
96	95	biimprcd 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ({x} ∈ ℘b → (℘g = ℘b → {x} ∈ ℘g))
97	96	con3d 125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({x} ∈ ℘b → (¬ {x} ∈ ℘g → ¬ ℘g = ℘b))
98	97	imp 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g) → ¬ ℘g = ℘b)
99	98	anim2i 552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((℘g ⊆ ℘b ∧ ({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g)) → (℘g ⊆ ℘b ∧ ¬ ℘g = ℘b))
100		dfpss2 3355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (℘g ⊊ ℘b ↔ (℘g ⊆ ℘b ∧ ¬ ℘g = ℘b))
101	99, 100	sylibr 203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((℘g ⊆ ℘b ∧ ({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g)) → ℘g ⊊ ℘b)
102		simp2ll 1022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → r ∈ Nn )
103	102	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → r ∈ Nn )
104		simp2rl 1024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → a ∈ r)
105	104	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → a ∈ r)
106		simprll 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → g ∈ r)
107		nnpweq 4524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((r ∈ Nn ∧ a ∈ r ∧ g ∈ r) → ∃u ∈ Nn (℘a ∈ u ∧ ℘g ∈ u))
108	103, 105, 106, 107	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → ∃u ∈ Nn (℘a ∈ u ∧ ℘g ∈ u))
109		simpr2l 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ℘a ∈ u)
110		simp3lr 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ℘a ∈ N)
111	110	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → ℘a ∈ N)
112	111	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ℘a ∈ N)
113		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (℘a ∈ (u ∩ N) ↔ (℘a ∈ u ∧ ℘a ∈ N))
114	109, 112, 113	sylanbrc 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ℘a ∈ (u ∩ N))
115		n0i 3556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (℘a ∈ (u ∩ N) → ¬ (u ∩ N) = ∅)
116	114, 115	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ¬ (u ∩ N) = ∅)
117		simpr1 961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → u ∈ Nn )
118		simp12l 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → N ∈ Nn )
119	118	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → N ∈ Nn )
120		nndisjeq 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((u ∈ Nn ∧ N ∈ Nn ) → ((u ∩ N) = ∅ ∨ u = N))
121	117, 119, 120	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ((u ∩ N) = ∅ ∨ u = N))
122		orel1 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (¬ (u ∩ N) = ∅ → (((u ∩ N) = ∅ ∨ u = N) → u = N))
123	116, 121, 122	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → u = N)
124		simp3rr 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ℘b ∈ Q)
125	124	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → ℘b ∈ Q)
126	125	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ℘b ∈ Q)
127		simp12r 1069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → Q ∈ Nn )
128	127	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → Q ∈ Nn )
129		elunii 3897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((℘b ∈ Q ∧ Q ∈ Nn ) → ℘b ∈ ∪ Nn )
130	126, 128, 129	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ℘b ∈ ∪ Nn )
131		df-fin 4381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ Fin = ∪ Nn
132	130, 131	syl6eleqr 2444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ℘b ∈ Fin )
133		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ b ∈ V
134	133	pwex 4330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ℘b ∈ V
135		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ g ∈ V
136	135	pwex 4330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ℘g ∈ V
137	134, 136	difex 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (℘b ∖ ℘g) ∈ V
138		difss 3394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (℘b ∖ ℘g) ⊆ ℘b
139		ssfin 4471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((℘b ∖ ℘g) ∈ V ∧ ℘b ∈ Fin ∧ (℘b ∖ ℘g) ⊆ ℘b) → (℘b ∖ ℘g) ∈ Fin )
140	137, 138, 139	mp3an13 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (℘b ∈ Fin → (℘b ∖ ℘g) ∈ Fin )
141	132, 140	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → (℘b ∖ ℘g) ∈ Fin )
142		elfin 4421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((℘b ∖ ℘g) ∈ Fin ↔ ∃n ∈ Nn (℘b ∖ ℘g) ∈ n)
143	125	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → ℘b ∈ Q)
144	143	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ℘b ∈ Q)
145		undif1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((℘b ∖ ℘g) ∪ ℘g) = (℘b ∪ ℘g)
146		uncom 3409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((℘b ∖ ℘g) ∪ ℘g) = (℘g ∪ (℘b ∖ ℘g))
147	145, 146	eqtr3i 2375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (℘b ∪ ℘g) = (℘g ∪ (℘b ∖ ℘g))
148		simp23 990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ℘g ⊊ ℘b)
149	148	pssssd 3367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ℘g ⊆ ℘b)
150		ssequn2 3437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (℘g ⊆ ℘b ↔ (℘b ∪ ℘g) = ℘b)
151	149, 150	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (℘b ∪ ℘g) = ℘b)
152	147, 151	syl5eqr 2399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (℘g ∪ (℘b ∖ ℘g)) = ℘b)
153		simp22r 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ℘g ∈ u)
154		simp3r 984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (℘b ∖ ℘g) ∈ n)
155		disjdif 3623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (℘g ∩ (℘b ∖ ℘g)) = ∅
156	155	a1i 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (℘g ∩ (℘b ∖ ℘g)) = ∅)
157		eladdci 4400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((℘g ∈ u ∧ (℘b ∖ ℘g) ∈ n ∧ (℘g ∩ (℘b ∖ ℘g)) = ∅) → (℘g ∪ (℘b ∖ ℘g)) ∈ (u +c n))
158	153, 154, 156, 157	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (℘g ∪ (℘b ∖ ℘g)) ∈ (u +c n))
159	152, 158	eqeltrrd 2428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ℘b ∈ (u +c n))
160		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (℘b ∈ (Q ∩ (u +c n)) ↔ (℘b ∈ Q ∧ ℘b ∈ (u +c n)))
161	144, 159, 160	sylanbrc 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ℘b ∈ (Q ∩ (u +c n)))
162		n0i 3556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (℘b ∈ (Q ∩ (u +c n)) → ¬ (Q ∩ (u +c n)) = ∅)
163	161, 162	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ¬ (Q ∩ (u +c n)) = ∅)
164	127	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → Q ∈ Nn )
165	164	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → Q ∈ Nn )
166		simp21 988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → u ∈ Nn )
167		simp3l 983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → n ∈ Nn )
168		nncaddccl 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((u ∈ Nn ∧ n ∈ Nn ) → (u +c n) ∈ Nn )
169	166, 167, 168	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (u +c n) ∈ Nn )
170		nndisjeq 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((Q ∈ Nn ∧ (u +c n) ∈ Nn ) → ((Q ∩ (u +c n)) = ∅ ∨ Q = (u +c n)))
171	165, 169, 170	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ((Q ∩ (u +c n)) = ∅ ∨ Q = (u +c n)))
172		orel1 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (¬ (Q ∩ (u +c n)) = ∅ → (((Q ∩ (u +c n)) = ∅ ∨ Q = (u +c n)) → Q = (u +c n)))
173	163, 171, 172	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → Q = (u +c n))
174		ne0i 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (℘g ∈ u → u ≠ ∅)
175	153, 174	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → u ≠ ∅)
176		df-pss 3262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (℘g ⊊ ℘b ↔ (℘g ⊆ ℘b ∧ ℘g ≠ ℘b))
177		ssdif0 3610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (℘b ⊆ ℘g ↔ (℘b ∖ ℘g) = ∅)
178		eqss 3288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (℘g = ℘b ↔ (℘g ⊆ ℘b ∧ ℘b ⊆ ℘g))
179	178	simplbi2 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (℘g ⊆ ℘b → (℘b ⊆ ℘g → ℘g = ℘b))
180	177, 179	syl5bir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (℘g ⊆ ℘b → ((℘b ∖ ℘g) = ∅ → ℘g = ℘b))
181	180	necon3d 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (℘g ⊆ ℘b → (℘g ≠ ℘b → (℘b ∖ ℘g) ≠ ∅))
182	181	imp 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((℘g ⊆ ℘b ∧ ℘g ≠ ℘b) → (℘b ∖ ℘g) ≠ ∅)
183	176, 182	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (℘g ⊊ ℘b → (℘b ∖ ℘g) ≠ ∅)
184	148, 183	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (℘b ∖ ℘g) ≠ ∅)
185		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (n = 0c → ((℘b ∖ ℘g) ∈ n ↔ (℘b ∖ ℘g) ∈ 0c))
186	185	biimpcd 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((℘b ∖ ℘g) ∈ n → (n = 0c → (℘b ∖ ℘g) ∈ 0c))
187		el0c 4422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((℘b ∖ ℘g) ∈ 0c ↔ (℘b ∖ ℘g) = ∅)
188	186, 187	syl6ib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((℘b ∖ ℘g) ∈ n → (n = 0c → (℘b ∖ ℘g) = ∅))
189	188	necon3ad 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((℘b ∖ ℘g) ∈ n → ((℘b ∖ ℘g) ≠ ∅ → ¬ n = 0c))
190	154, 184, 189	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ¬ n = 0c)
191		nnc0suc 4413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (n ∈ Nn ↔ (n = 0c ∨ ∃m ∈ Nn n = (m +c 1c)))
192	167, 191	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (n = 0c ∨ ∃m ∈ Nn n = (m +c 1c)))
193		orel1 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (¬ n = 0c → ((n = 0c ∨ ∃m ∈ Nn n = (m +c 1c)) → ∃m ∈ Nn n = (m +c 1c)))
194	190, 192, 193	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ∃m ∈ Nn n = (m +c 1c))
195		addceq2 4385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (n = (m +c 1c) → (u +c n) = (u +c (m +c 1c)))
196		addcass 4416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((u +c m) +c 1c) = (u +c (m +c 1c))
197	195, 196	syl6eqr 2403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (n = (m +c 1c) → (u +c n) = ((u +c m) +c 1c))
198	197	reximi 2722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (∃m ∈ Nn n = (m +c 1c) → ∃m ∈ Nn (u +c n) = ((u +c m) +c 1c))
199	194, 198	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ∃m ∈ Nn (u +c n) = ((u +c m) +c 1c))
200		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ u ∈ V
201		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ n ∈ V
202	200, 201	addcex 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (u +c n) ∈ V
203		opkltfing 4450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((u ∈ V ∧ (u +c n) ∈ V) → (⟪u, (u +c n)⟫ ∈ <fin ↔ (u ≠ ∅ ∧ ∃m ∈ Nn (u +c n) = ((u +c m) +c 1c))))
204	200, 202, 203	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (⟪u, (u +c n)⟫ ∈ <fin ↔ (u ≠ ∅ ∧ ∃m ∈ Nn (u +c n) = ((u +c m) +c 1c)))
205	175, 199, 204	sylanbrc 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ⟪u, (u +c n)⟫ ∈ <fin )
206		opkeq2 4061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (Q = (u +c n) → ⟪u, Q⟫ = ⟪u, (u +c n)⟫)
207	206	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (Q = (u +c n) → (⟪u, Q⟫ ∈ <fin ↔ ⟪u, (u +c n)⟫ ∈ <fin ))
208	205, 207	syl5ibrcom 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → (Q = (u +c n) → ⟪u, Q⟫ ∈ <fin ))
209	173, 208	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ⟪u, Q⟫ ∈ <fin )
210	209	3expa 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) → ⟪u, Q⟫ ∈ <fin )
211	210	exp32 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → (n ∈ Nn → ((℘b ∖ ℘g) ∈ n → ⟪u, Q⟫ ∈ <fin )))
212	211	rexlimdv 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → (∃n ∈ Nn (℘b ∖ ℘g) ∈ n → ⟪u, Q⟫ ∈ <fin ))
213	142, 212	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ((℘b ∖ ℘g) ∈ Fin → ⟪u, Q⟫ ∈ <fin ))
214	141, 213	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ⟪u, Q⟫ ∈ <fin )
215		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (u = N → ⟪u, Q⟫ = ⟪N, Q⟫)
216	215	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (u = N → (⟪u, Q⟫ ∈ <fin ↔ ⟪N, Q⟫ ∈ <fin ))
217	214, 216	syl5ibcom 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → (u = N → ⟪N, Q⟫ ∈ <fin ))
218	123, 217	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) ∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) → ⟪N, Q⟫ ∈ <fin )
219	218	3exp2 1169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (u ∈ Nn → ((℘a ∈ u ∧ ℘g ∈ u) → (℘g ⊊ ℘b → ⟪N, Q⟫ ∈ <fin ))))
220	219	rexlimdv 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (∃u ∈ Nn (℘a ∈ u ∧ ℘g ∈ u) → (℘g ⊊ ℘b → ⟪N, Q⟫ ∈ <fin )))
221	108, 220	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (℘g ⊊ ℘b → ⟪N, Q⟫ ∈ <fin ))
222	101, 221	syl5 28	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → ((℘g ⊆ ℘b ∧ ({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g)) → ⟪N, Q⟫ ∈ <fin ))
223	94, 222	mpand 656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g) → ⟪N, Q⟫ ∈ <fin ))
224	87, 223	syl5bir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → ((x ∈ b ∧ ¬ x ∈ g) → ⟪N, Q⟫ ∈ <fin ))
225	82, 224	syld 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (x ∈ d → ⟪N, Q⟫ ∈ <fin ))
226	225	exlimdv 1636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (∃x x ∈ d → ⟪N, Q⟫ ∈ <fin ))
227	72, 226	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → (d ≠ ∅ → ⟪N, Q⟫ ∈ <fin ))
228	71, 227	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) ∧ ((g ∈ r ∧ d ∈ (t +c 1c)) ∧ ((g ∩ d) = ∅ ∧ b = (g ∪ d)))) → ⟪N, Q⟫ ∈ <fin )
229	228	exp32 588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → ((g ∈ r ∧ d ∈ (t +c 1c)) → (((g ∩ d) = ∅ ∧ b = (g ∪ d)) → ⟪N, Q⟫ ∈ <fin )))
230	229	rexlimdvv 2745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → (∃g ∈ r ∃d ∈ (t +c 1c)((g ∩ d) = ∅ ∧ b = (g ∪ d)) → ⟪N, Q⟫ ∈ <fin ))
231	64, 230	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → (b ∈ (r +c (t +c 1c)) → ⟪N, Q⟫ ∈ <fin ))
232	63, 231	mpd 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → ⟪N, Q⟫ ∈ <fin )
233	232	3expa 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c))) → ⟪N, Q⟫ ∈ <fin )
234	233	exp32 588	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → (t ∈ Nn → (s = ((r +c t) +c 1c) → ⟪N, Q⟫ ∈ <fin )))
235	234	rexlimdv 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → (∃t ∈ Nn s = ((r +c t) +c 1c) → ⟪N, Q⟫ ∈ <fin ))
236	235	adantld 453	. . . . . . . . . . . . . . . . 17 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ((r ≠ ∅ ∧ ∃t ∈ Nn s = ((r +c t) +c 1c)) → ⟪N, Q⟫ ∈ <fin ))
237	58, 236	sylbid 206	. . . . . . . . . . . . . . . 16 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → (⟪r, s⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))
238	56, 237	sylbird 226	. . . . . . . . . . . . . . 15 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → (⟪ Tfin r, Tfin s⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))
239		opkeq12 4062	. . . . . . . . . . . . . . . . 17 ⊢ ((M = Tfin r ∧ P = Tfin s) → ⟪M, P⟫ = ⟪ Tfin r, Tfin s⟫)
240	239	eleq1d 2419	. . . . . . . . . . . . . . . 16 ⊢ ((M = Tfin r ∧ P = Tfin s) → (⟪M, P⟫ ∈ <fin ↔ ⟪ Tfin r, Tfin s⟫ ∈ <fin ))
241	240	imbi1d 308	. . . . . . . . . . . . . . 15 ⊢ ((M = Tfin r ∧ P = Tfin s) → ((⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ) ↔ (⟪ Tfin r, Tfin s⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin )))
242	238, 241	syl5ibrcom 213	. . . . . . . . . . . . . 14 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → ((M = Tfin r ∧ P = Tfin s) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin )))
243	35, 54, 242	mp2and 660	. . . . . . . . . . . . 13 ⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))
244	243	exp32 588	. . . . . . . . . . . 12 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ((r ∈ Nn ∧ s ∈ Nn ) → ((a ∈ r ∧ b ∈ s) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))))
245	16, 244	syl7 63	. . . . . . . . . . 11 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ((r ∈ Nn ∧ s ∈ Nn ) → (((a ∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))))
246	245	rexlimdvv 2745	. . . . . . . . . 10 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → (∃r ∈ Nn ∃s ∈ Nn ((a ∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin )))
247	13, 246	syl5bir 209	. . . . . . . . 9 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → ((∃r ∈ Nn (a ∈ r ∧ a ∈ r) ∧ ∃s ∈ Nn (b ∈ s ∧ b ∈ s)) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin )))
248	8, 12, 247	mp2and 660	. . . . . . . 8 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))
249	248	3expia 1153	. . . . . . 7 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn )) → (((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q)) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin )))
250	249	exlimdvv 1637	. . . . . 6 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn )) → (∃a∃b((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q)) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin )))
251	4, 250	syl5bir 209	. . . . 5 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn )) → ((∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q)) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin )))
252	251	3impia 1148	. . . 4 ⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ (∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))
253	3, 252	sylbir 204	. . 3 ⊢ (((M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)) ∧ (P ∈ Nn ∧ Q ∈ Nn ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))
254	1, 2, 253	syl2anb 465	. 2 ⊢ (( Sfin (M, N) ∧ Sfin (P, Q)) → (⟪M, P⟫ ∈ <fin → ⟪N, Q⟫ ∈ <fin ))
255	254	imp 418	1 ⊢ ((( Sfin (M, N) ∧ Sfin (P, Q)) ∧ ⟪M, P⟫ ∈ <fin ) → ⟪N, Q⟫ ∈ <fin )

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710   ≠ wne 2517  ∀wral 2615  ∃wrex 2616  Vcvv 2860   ∖ cdif 3207   ∪ cun 3208   ∩ cin 3209   ⊆ wss 3258   ⊊ wpss 3259  ∅c0 3551  ℘cpw 3723  {csn 3738  ∪cuni 3892  ⟪copk 4058  1_cc1c 4135  ℘₁cpw1 4136   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376   Fin cfin 4377   <_fin cltfin 4434   T_fin ctfin 4436   S_fin wsfin 4439

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-tfin 4444  df-sfin 4447

This theorem is used by:  sfin111  4537  vfinspsslem1  4551