marypha1lem

Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015)

		Ref	Expression
	Assertion	marypha1lem	$⊢ A \in Fin \to (b \in Fin \to \forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists e \in 𝒫 c e : A \underset{1-1}{⟶} V))$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$⊢ a = f \to a \times b = f \times b$
2	1	pweqd	$⊢ a = f \to 𝒫 (a \times b) = 𝒫 (f \times b)$
3		pweq	$⊢ a = f \to 𝒫 a = 𝒫 f$
4	3	raleqdv	$⊢ a = f \to (\forall d \in 𝒫 a d ≼ c [d] \leftrightarrow \forall d \in 𝒫 f d ≼ c [d])$
5		f1eq2	$⊢ a = f \to (e : a \underset{1-1}{⟶} V \leftrightarrow e : f \underset{1-1}{⟶} V)$
6	5	rexbidv	$⊢ a = f \to (\exists e \in 𝒫 c e : a \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)$
7	4 6	imbi12d	$⊢ a = f \to ((\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V))$
8	2 7	raleqbidv	$⊢ a = f \to (\forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow \forall c \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V))$
9	8	imbi2d	$⊢ a = f \to ((b \in Fin \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \leftrightarrow (b \in Fin \to \forall c \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)))$
10		xpeq1	$⊢ a = A \to a \times b = A \times b$
11	10	pweqd	$⊢ a = A \to 𝒫 (a \times b) = 𝒫 (A \times b)$
12		pweq	$⊢ a = A \to 𝒫 a = 𝒫 A$
13	12	raleqdv	$⊢ a = A \to (\forall d \in 𝒫 a d ≼ c [d] \leftrightarrow \forall d \in 𝒫 A d ≼ c [d])$
14		f1eq2	$⊢ a = A \to (e : a \underset{1-1}{⟶} V \leftrightarrow e : A \underset{1-1}{⟶} V)$
15	14	rexbidv	$⊢ a = A \to (\exists e \in 𝒫 c e : a \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 c e : A \underset{1-1}{⟶} V)$
16	13 15	imbi12d	$⊢ a = A \to ((\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 A d ≼ c [d] \to \exists e \in 𝒫 c e : A \underset{1-1}{⟶} V))$
17	11 16	raleqbidv	$⊢ a = A \to (\forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow \forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists e \in 𝒫 c e : A \underset{1-1}{⟶} V))$
18	17	imbi2d	$⊢ a = A \to ((b \in Fin \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \leftrightarrow (b \in Fin \to \forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists e \in 𝒫 c e : A \underset{1-1}{⟶} V)))$
19		bi2.04	$⊢ (a \subset f \to (b \in Fin \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \leftrightarrow (b \in Fin \to (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)))$
20	19	albii	$⊢ \forall a (a \subset f \to (b \in Fin \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \leftrightarrow \forall a (b \in Fin \to (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)))$
21		19.21v	$⊢ \forall a (b \in Fin \to (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \leftrightarrow (b \in Fin \to \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)))$
22	20 21	bitri	$⊢ \forall a (a \subset f \to (b \in Fin \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \leftrightarrow (b \in Fin \to \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)))$
23		0elpw	$⊢ \emptyset \in 𝒫 g$
24		f10	$⊢ \emptyset : \emptyset \underset{1-1}{⟶} V$
25		f1eq1	$⊢ e = \emptyset \to (e : \emptyset \underset{1-1}{⟶} V \leftrightarrow \emptyset : \emptyset \underset{1-1}{⟶} V)$
26	25	rspcev	$⊢ (\emptyset \in 𝒫 g \land \emptyset : \emptyset \underset{1-1}{⟶} V) \to \exists e \in 𝒫 g e : \emptyset \underset{1-1}{⟶} V$
27	23 24 26	mp2an	$⊢ \exists e \in 𝒫 g e : \emptyset \underset{1-1}{⟶} V$
28		f1eq2	$⊢ f = \emptyset \to (e : f \underset{1-1}{⟶} V \leftrightarrow e : \emptyset \underset{1-1}{⟶} V)$
29	28	rexbidv	$⊢ f = \emptyset \to (\exists e \in 𝒫 g e : f \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 g e : \emptyset \underset{1-1}{⟶} V)$
30	27 29	mpbiri	$⊢ f = \emptyset \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
31	30	a1i	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to (f = \emptyset \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
32		n0	$⊢ f \neq \emptyset \leftrightarrow \exists i i \in f$
33		snelpwi	$⊢ i \in f \to \{i\} \in 𝒫 f$
34		id	$⊢ d = \{i\} \to d = \{i\}$
35		imaeq2	$⊢ d = \{i\} \to g [d] = g [\{i\}]$
36	34 35	breq12d	$⊢ d = \{i\} \to (d ≼ g [d] \leftrightarrow \{i\} ≼ g [\{i\}])$
37	36	rspcva	$⊢ (\{i\} \in 𝒫 f \land \forall d \in 𝒫 f d ≼ g [d]) \to \{i\} ≼ g [\{i\}]$
38		vex	$⊢ i \in V$
39	38	snnz	$⊢ \{i\} \neq \emptyset$
40		snex	$⊢ \{i\} \in V$
41	40	0sdom	$⊢ \emptyset ≺ \{i\} \leftrightarrow \{i\} \neq \emptyset$
42	39 41	mpbir	$⊢ \emptyset ≺ \{i\}$
43		sdomdomtr	$⊢ (\emptyset ≺ \{i\} \land \{i\} ≼ g [\{i\}]) \to \emptyset ≺ g [\{i\}]$
44	42 43	mpan	$⊢ \{i\} ≼ g [\{i\}] \to \emptyset ≺ g [\{i\}]$
45		vex	$⊢ g \in V$
46	45	imaex	$⊢ g [\{i\}] \in V$
47	46	0sdom	$⊢ \emptyset ≺ g [\{i\}] \leftrightarrow g [\{i\}] \neq \emptyset$
48	44 47	sylib	$⊢ \{i\} ≼ g [\{i\}] \to g [\{i\}] \neq \emptyset$
49	37 48	syl	$⊢ (\{i\} \in 𝒫 f \land \forall d \in 𝒫 f d ≼ g [d]) \to g [\{i\}] \neq \emptyset$
50	49	expcom	$⊢ \forall d \in 𝒫 f d ≼ g [d] \to (\{i\} \in 𝒫 f \to g [\{i\}] \neq \emptyset)$
51	33 50	syl5	$⊢ \forall d \in 𝒫 f d ≼ g [d] \to (i \in f \to g [\{i\}] \neq \emptyset)$
52	51	adantl	$⊢ (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d]) \to (i \in f \to g [\{i\}] \neq \emptyset)$
53	52	ad2antlr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to (i \in f \to g [\{i\}] \neq \emptyset)$
54	53	impr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f)) \to g [\{i\}] \neq \emptyset$
55		n0	$⊢ g [\{i\}] \neq \emptyset \leftrightarrow \exists j j \in g [\{i\}]$
56	54 55	sylib	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f)) \to \exists j j \in g [\{i\}]$
57	45	imaex	$⊢ g [c] \in V$
58	57	difexi	$⊢ g [c] ∖ \{j\} \in V$
59	58	0dom	$⊢ \emptyset ≼ (g [c] ∖ \{j\})$
60		breq1	$⊢ c = \emptyset \to (c ≼ (g [c] ∖ \{j\}) \leftrightarrow \emptyset ≼ (g [c] ∖ \{j\}))$
61	59 60	mpbiri	$⊢ c = \emptyset \to c ≼ (g [c] ∖ \{j\})$
62	61	a1i	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land c \in 𝒫 (f ∖ \{i\})) \to (c = \emptyset \to c ≼ (g [c] ∖ \{j\}))$
63		simpll	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])$
64		elpwi	$⊢ c \in 𝒫 (f ∖ \{i\}) \to c \subseteq f ∖ \{i\}$
65	64	ad2antrl	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to c \subseteq f ∖ \{i\}$
66		difsnpss	$⊢ i \in f \leftrightarrow f ∖ \{i\} \subset f$
67	66	biimpi	$⊢ i \in f \to f ∖ \{i\} \subset f$
68	67	ad2antlr	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to f ∖ \{i\} \subset f$
69	65 68	sspsstrd	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to c \subset f$
70		simprr	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to c \neq \emptyset$
71	69 70	jca	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to (c \subset f \land c \neq \emptyset)$
72		psseq1	$⊢ h = c \to (h \subset f \leftrightarrow c \subset f)$
73		neeq1	$⊢ h = c \to (h \neq \emptyset \leftrightarrow c \neq \emptyset)$
74	72 73	anbi12d	$⊢ h = c \to ((h \subset f \land h \neq \emptyset) \leftrightarrow (c \subset f \land c \neq \emptyset))$
75		id	$⊢ h = c \to h = c$
76		imaeq2	$⊢ h = c \to g [h] = g [c]$
77	75 76	breq12d	$⊢ h = c \to (h ≺ g [h] \leftrightarrow c ≺ g [c])$
78	74 77	imbi12d	$⊢ h = c \to (((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \leftrightarrow ((c \subset f \land c \neq \emptyset) \to c ≺ g [c]))$
79	78	spvv	$⊢ \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \to ((c \subset f \land c \neq \emptyset) \to c ≺ g [c])$
80	63 71 79	sylc	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to c ≺ g [c]$
81		domdifsn	$⊢ c ≺ g [c] \to c ≼ (g [c] ∖ \{j\})$
82	80 81	syl	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land (c \in 𝒫 (f ∖ \{i\}) \land c \neq \emptyset)) \to c ≼ (g [c] ∖ \{j\})$
83	82	expr	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land c \in 𝒫 (f ∖ \{i\})) \to (c \neq \emptyset \to c ≼ (g [c] ∖ \{j\}))$
84	62 83	pm2.61dne	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f) \land c \in 𝒫 (f ∖ \{i\})) \to c ≼ (g [c] ∖ \{j\})$
85	84	adantlrr	$⊢ ((\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}])) \land c \in 𝒫 (f ∖ \{i\})) \to c ≼ (g [c] ∖ \{j\})$
86	85	adantll	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \land c \in 𝒫 (f ∖ \{i\})) \to c ≼ (g [c] ∖ \{j\})$
87		df-ss	$⊢ c \subseteq f ∖ \{i\} \leftrightarrow c \cap (f ∖ \{i\}) = c$
88	64 87	sylib	$⊢ c \in 𝒫 (f ∖ \{i\}) \to c \cap (f ∖ \{i\}) = c$
89	88	imaeq2d	$⊢ c \in 𝒫 (f ∖ \{i\}) \to g [c \cap (f ∖ \{i\})] = g [c]$
90	89	ineq1d	$⊢ c \in 𝒫 (f ∖ \{i\}) \to g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\}) = g [c] \cap (b ∖ \{j\})$
91	90	adantl	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \land c \in 𝒫 (f ∖ \{i\})) \to g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\}) = g [c] \cap (b ∖ \{j\})$
92		indif2	$⊢ g [c] \cap (b ∖ \{j\}) = (g [c] \cap b) ∖ \{j\}$
93		imassrn	$⊢ g [c] \subseteq ran g$
94		elpwi	$⊢ g \in 𝒫 (f \times b) \to g \subseteq f \times b$
95		rnss	$⊢ g \subseteq f \times b \to ran g \subseteq ran (f \times b)$
96		rnxpss	$⊢ ran (f \times b) \subseteq b$
97	95 96	sstrdi	$⊢ g \subseteq f \times b \to ran g \subseteq b$
98	94 97	syl	$⊢ g \in 𝒫 (f \times b) \to ran g \subseteq b$
99	93 98	sstrid	$⊢ g \in 𝒫 (f \times b) \to g [c] \subseteq b$
100		df-ss	$⊢ g [c] \subseteq b \leftrightarrow g [c] \cap b = g [c]$
101	99 100	sylib	$⊢ g \in 𝒫 (f \times b) \to g [c] \cap b = g [c]$
102	101	difeq1d	$⊢ g \in 𝒫 (f \times b) \to (g [c] \cap b) ∖ \{j\} = g [c] ∖ \{j\}$
103	102	ad2antrl	$⊢ ((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \to (g [c] \cap b) ∖ \{j\} = g [c] ∖ \{j\}$
104	92 103	syl5eq	$⊢ ((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \to g [c] \cap (b ∖ \{j\}) = g [c] ∖ \{j\}$
105	104	ad2antrr	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \land c \in 𝒫 (f ∖ \{i\})) \to g [c] \cap (b ∖ \{j\}) = g [c] ∖ \{j\}$
106	91 105	eqtrd	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \land c \in 𝒫 (f ∖ \{i\})) \to g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\}) = g [c] ∖ \{j\}$
107	86 106	breqtrrd	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \land c \in 𝒫 (f ∖ \{i\})) \to c ≼ (g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\}))$
108	107	ralrimiva	$⊢ (((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \forall c \in 𝒫 (f ∖ \{i\}) c ≼ (g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\}))$
109		id	$⊢ c = d \to c = d$
110		imainrect	$⊢ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [c] = g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\})$
111		imaeq2	$⊢ c = d \to (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [c] = (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d]$
112	110 111	eqtr3id	$⊢ c = d \to g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\}) = (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d]$
113	109 112	breq12d	$⊢ c = d \to (c ≼ (g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\})) \leftrightarrow d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d])$
114	113	cbvralvw	$⊢ \forall c \in 𝒫 (f ∖ \{i\}) c ≼ (g [c \cap (f ∖ \{i\})] \cap (b ∖ \{j\})) \leftrightarrow \forall d \in 𝒫 (f ∖ \{i\}) d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d]$
115	108 114	sylib	$⊢ (((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \forall d \in 𝒫 (f ∖ \{i\}) d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d]$
116	115	adantllr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \forall d \in 𝒫 (f ∖ \{i\}) d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d]$
117		inss2	$⊢ g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \subseteq (f ∖ \{i\}) \times (b ∖ \{j\})$
118		difss	$⊢ b ∖ \{j\} \subseteq b$
119		xpss2	$⊢ b ∖ \{j\} \subseteq b \to (f ∖ \{i\}) \times (b ∖ \{j\}) \subseteq (f ∖ \{i\}) \times b$
120	118 119	ax-mp	$⊢ (f ∖ \{i\}) \times (b ∖ \{j\}) \subseteq (f ∖ \{i\}) \times b$
121	117 120	sstri	$⊢ g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \subseteq (f ∖ \{i\}) \times b$
122	45	inex1	$⊢ g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \in V$
123	122	elpw	$⊢ g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \in 𝒫 ((f ∖ \{i\}) \times b) \leftrightarrow g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \subseteq (f ∖ \{i\}) \times b$
124	121 123	mpbir	$⊢ g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \in 𝒫 ((f ∖ \{i\}) \times b)$
125		simpllr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))$
126	67	adantr	$⊢ (i \in f \land j \in g [\{i\}]) \to f ∖ \{i\} \subset f$
127	126	ad2antll	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to f ∖ \{i\} \subset f$
128		vex	$⊢ f \in V$
129	128	difexi	$⊢ f ∖ \{i\} \in V$
130		psseq1	$⊢ a = f ∖ \{i\} \to (a \subset f \leftrightarrow f ∖ \{i\} \subset f)$
131		xpeq1	$⊢ a = f ∖ \{i\} \to a \times b = (f ∖ \{i\}) \times b$
132	131	pweqd	$⊢ a = f ∖ \{i\} \to 𝒫 (a \times b) = 𝒫 ((f ∖ \{i\}) \times b)$
133		pweq	$⊢ a = f ∖ \{i\} \to 𝒫 a = 𝒫 (f ∖ \{i\})$
134	133	raleqdv	$⊢ a = f ∖ \{i\} \to (\forall d \in 𝒫 a d ≼ c [d] \leftrightarrow \forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d])$
135		f1eq2	$⊢ a = f ∖ \{i\} \to (e : a \underset{1-1}{⟶} V \leftrightarrow e : f ∖ \{i\} \underset{1-1}{⟶} V)$
136	135	rexbidv	$⊢ a = f ∖ \{i\} \to (\exists e \in 𝒫 c e : a \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V)$
137	134 136	imbi12d	$⊢ a = f ∖ \{i\} \to ((\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V))$
138	132 137	raleqbidv	$⊢ a = f ∖ \{i\} \to (\forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow \forall c \in 𝒫 ((f ∖ \{i\}) \times b) (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V))$
139	130 138	imbi12d	$⊢ a = f ∖ \{i\} \to ((a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \leftrightarrow (f ∖ \{i\} \subset f \to \forall c \in 𝒫 ((f ∖ \{i\}) \times b) (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V)))$
140	129 139	spcv	$⊢ \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \to (f ∖ \{i\} \subset f \to \forall c \in 𝒫 ((f ∖ \{i\}) \times b) (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V))$
141	125 127 140	sylc	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \forall c \in 𝒫 ((f ∖ \{i\}) \times b) (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V)$
142		imaeq1	$⊢ c = g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \to c [d] = (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d]$
143	142	breq2d	$⊢ c = g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \to (d ≼ c [d] \leftrightarrow d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d])$
144	143	ralbidv	$⊢ c = g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \to (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \leftrightarrow \forall d \in 𝒫 (f ∖ \{i\}) d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d])$
145		pweq	$⊢ c = g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \to 𝒫 c = 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})))$
146	145	rexeqdv	$⊢ c = g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \to (\exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) e : f ∖ \{i\} \underset{1-1}{⟶} V)$
147	144 146	imbi12d	$⊢ c = g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \to ((\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d] \to \exists e \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) e : f ∖ \{i\} \underset{1-1}{⟶} V))$
148	147	rspcva	$⊢ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \in 𝒫 ((f ∖ \{i\}) \times b) \land \forall c \in 𝒫 ((f ∖ \{i\}) \times b) (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ \{i\} \underset{1-1}{⟶} V)) \to (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d] \to \exists e \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) e : f ∖ \{i\} \underset{1-1}{⟶} V)$
149	124 141 148	sylancr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to (\forall d \in 𝒫 (f ∖ \{i\}) d ≼ (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) [d] \to \exists e \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) e : f ∖ \{i\} \underset{1-1}{⟶} V)$
150	116 149	mpd	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \exists e \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) e : f ∖ \{i\} \underset{1-1}{⟶} V$
151		f1eq1	$⊢ e = k \to (e : f ∖ \{i\} \underset{1-1}{⟶} V \leftrightarrow k : f ∖ \{i\} \underset{1-1}{⟶} V)$
152	151	cbvrexvw	$⊢ \exists e \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) e : f ∖ \{i\} \underset{1-1}{⟶} V \leftrightarrow \exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V$
153	150 152	sylib	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V$
154		vex	$⊢ j \in V$
155	38 154	elimasn	$⊢ j \in g [\{i\}] \leftrightarrow ⟨i, j⟩ \in g$
156	155	biimpi	$⊢ j \in g [\{i\}] \to ⟨i, j⟩ \in g$
157	156	snssd	$⊢ j \in g [\{i\}] \to \{⟨i, j⟩\} \subseteq g$
158	157	ad2antlr	$⊢ ((i \in f \land j \in g [\{i\}]) \land k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})))) \to \{⟨i, j⟩\} \subseteq g$
159		elpwi	$⊢ k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \to k \subseteq g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))$
160		inss1	$⊢ g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})) \subseteq g$
161	159 160	sstrdi	$⊢ k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \to k \subseteq g$
162	161	adantl	$⊢ ((i \in f \land j \in g [\{i\}]) \land k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})))) \to k \subseteq g$
163	158 162	unssd	$⊢ ((i \in f \land j \in g [\{i\}]) \land k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})))) \to \{⟨i, j⟩\} \cup k \subseteq g$
164	45	elpw2	$⊢ \{⟨i, j⟩\} \cup k \in 𝒫 g \leftrightarrow \{⟨i, j⟩\} \cup k \subseteq g$
165	163 164	sylibr	$⊢ ((i \in f \land j \in g [\{i\}]) \land k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\})))) \to \{⟨i, j⟩\} \cup k \in 𝒫 g$
166	165	ad2ant2lr	$⊢ ((g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \land (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V)) \to \{⟨i, j⟩\} \cup k \in 𝒫 g$
167	38 154	f1osn	$⊢ \{⟨i, j⟩\} : \{i\} \underset{1-1 onto}{⟶} \{j\}$
168	167	a1i	$⊢ (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V) \to \{⟨i, j⟩\} : \{i\} \underset{1-1 onto}{⟶} \{j\}$
169		f1f1orn	$⊢ k : f ∖ \{i\} \underset{1-1}{⟶} V \to k : f ∖ \{i\} \underset{1-1 onto}{⟶} ran k$
170	169	adantl	$⊢ (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V) \to k : f ∖ \{i\} \underset{1-1 onto}{⟶} ran k$
171		disjdif	$⊢ \{i\} \cap (f ∖ \{i\}) = \emptyset$
172	171	a1i	$⊢ (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V) \to \{i\} \cap (f ∖ \{i\}) = \emptyset$
173		incom	$⊢ \{j\} \cap ran k = ran k \cap \{j\}$
174	159 117	sstrdi	$⊢ k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \to k \subseteq (f ∖ \{i\}) \times (b ∖ \{j\})$
175		rnss	$⊢ k \subseteq (f ∖ \{i\}) \times (b ∖ \{j\}) \to ran k \subseteq ran ((f ∖ \{i\}) \times (b ∖ \{j\}))$
176		rnxpss	$⊢ ran ((f ∖ \{i\}) \times (b ∖ \{j\})) \subseteq b ∖ \{j\}$
177	175 176	sstrdi	$⊢ k \subseteq (f ∖ \{i\}) \times (b ∖ \{j\}) \to ran k \subseteq b ∖ \{j\}$
178	174 177	syl	$⊢ k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \to ran k \subseteq b ∖ \{j\}$
179		disjdifr	$⊢ (b ∖ \{j\}) \cap \{j\} = \emptyset$
180		ssdisj	$⊢ (ran k \subseteq b ∖ \{j\} \land (b ∖ \{j\}) \cap \{j\} = \emptyset) \to ran k \cap \{j\} = \emptyset$
181	178 179 180	sylancl	$⊢ k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \to ran k \cap \{j\} = \emptyset$
182	173 181	syl5eq	$⊢ k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \to \{j\} \cap ran k = \emptyset$
183	182	adantr	$⊢ (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V) \to \{j\} \cap ran k = \emptyset$
184		f1oun	$⊢ ((\{⟨i, j⟩\} : \{i\} \underset{1-1 onto}{⟶} \{j\} \land k : f ∖ \{i\} \underset{1-1 onto}{⟶} ran k) \land (\{i\} \cap (f ∖ \{i\}) = \emptyset \land \{j\} \cap ran k = \emptyset)) \to (\{⟨i, j⟩\} \cup k) : \{i\} \cup (f ∖ \{i\}) \underset{1-1 onto}{⟶} \{j\} \cup ran k$
185	168 170 172 183 184	syl22anc	$⊢ (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V) \to (\{⟨i, j⟩\} \cup k) : \{i\} \cup (f ∖ \{i\}) \underset{1-1 onto}{⟶} \{j\} \cup ran k$
186	185	adantl	$⊢ ((g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \land (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V)) \to (\{⟨i, j⟩\} \cup k) : \{i\} \cup (f ∖ \{i\}) \underset{1-1 onto}{⟶} \{j\} \cup ran k$
187		snssi	$⊢ i \in f \to \{i\} \subseteq f$
188	187	ad2antrl	$⊢ (g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \to \{i\} \subseteq f$
189		undif	$⊢ \{i\} \subseteq f \leftrightarrow \{i\} \cup (f ∖ \{i\}) = f$
190	188 189	sylib	$⊢ (g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \to \{i\} \cup (f ∖ \{i\}) = f$
191	190	f1oeq2d	$⊢ (g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \to ((\{⟨i, j⟩\} \cup k) : \{i\} \cup (f ∖ \{i\}) \underset{1-1 onto}{⟶} \{j\} \cup ran k \leftrightarrow (\{⟨i, j⟩\} \cup k) : f \underset{1-1 onto}{⟶} \{j\} \cup ran k)$
192	191	adantr	$⊢ ((g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \land (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V)) \to ((\{⟨i, j⟩\} \cup k) : \{i\} \cup (f ∖ \{i\}) \underset{1-1 onto}{⟶} \{j\} \cup ran k \leftrightarrow (\{⟨i, j⟩\} \cup k) : f \underset{1-1 onto}{⟶} \{j\} \cup ran k)$
193	186 192	mpbid	$⊢ ((g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \land (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V)) \to (\{⟨i, j⟩\} \cup k) : f \underset{1-1 onto}{⟶} \{j\} \cup ran k$
194		f1of1	$⊢ (\{⟨i, j⟩\} \cup k) : f \underset{1-1 onto}{⟶} \{j\} \cup ran k \to (\{⟨i, j⟩\} \cup k) : f \underset{1-1}{⟶} \{j\} \cup ran k$
195		ssv	$⊢ \{j\} \cup ran k \subseteq V$
196		f1ss	$⊢ ((\{⟨i, j⟩\} \cup k) : f \underset{1-1}{⟶} \{j\} \cup ran k \land \{j\} \cup ran k \subseteq V) \to (\{⟨i, j⟩\} \cup k) : f \underset{1-1}{⟶} V$
197	194 195 196	sylancl	$⊢ (\{⟨i, j⟩\} \cup k) : f \underset{1-1 onto}{⟶} \{j\} \cup ran k \to (\{⟨i, j⟩\} \cup k) : f \underset{1-1}{⟶} V$
198	193 197	syl	$⊢ ((g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \land (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V)) \to (\{⟨i, j⟩\} \cup k) : f \underset{1-1}{⟶} V$
199		f1eq1	$⊢ e = \{⟨i, j⟩\} \cup k \to (e : f \underset{1-1}{⟶} V \leftrightarrow (\{⟨i, j⟩\} \cup k) : f \underset{1-1}{⟶} V)$
200	199	rspcev	$⊢ (\{⟨i, j⟩\} \cup k \in 𝒫 g \land (\{⟨i, j⟩\} \cup k) : f \underset{1-1}{⟶} V) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
201	166 198 200	syl2anc	$⊢ ((g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \land (k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) \land k : f ∖ \{i\} \underset{1-1}{⟶} V)) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
202	201	rexlimdvaa	$⊢ (g \in 𝒫 (f \times b) \land (i \in f \land j \in g [\{i\}])) \to (\exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
203	202	ex	$⊢ g \in 𝒫 (f \times b) \to ((i \in f \land j \in g [\{i\}]) \to (\exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V))$
204	203	adantr	$⊢ (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d]) \to ((i \in f \land j \in g [\{i\}]) \to (\exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V))$
205	204	ad2antlr	$⊢ (((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to ((i \in f \land j \in g [\{i\}]) \to (\exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V))$
206	205	impr	$⊢ (((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to (\exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
207	206	adantllr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to (\exists k \in 𝒫 (g \cap ((f ∖ \{i\}) \times (b ∖ \{j\}))) k : f ∖ \{i\} \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
208	153 207	mpd	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land (i \in f \land j \in g [\{i\}]))) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
209	208	expr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to ((i \in f \land j \in g [\{i\}]) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
210	209	expd	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to (i \in f \to (j \in g [\{i\}] \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V))$
211	210	impr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f)) \to (j \in g [\{i\}] \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
212	211	exlimdv	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f)) \to (\exists j j \in g [\{i\}] \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
213	56 212	mpd	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land (\forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h]) \land i \in f)) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
214	213	expr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to (i \in f \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
215	214	exlimdv	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to (\exists i i \in f \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
216	32 215	syl5bi	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to (f \neq \emptyset \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
217	31 216	pm2.61dne	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
218		exanali	$⊢ \exists h ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h]) \leftrightarrow \neg \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])$
219		simprll	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to h \subset f$
220		pssss	$⊢ h \subset f \to h \subseteq f$
221	219 220	syl	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to h \subseteq f$
222	221	sspwd	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to 𝒫 h \subseteq 𝒫 f$
223		simplrr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall d \in 𝒫 f d ≼ g [d]$
224		ssralv	$⊢ 𝒫 h \subseteq 𝒫 f \to (\forall d \in 𝒫 f d ≼ g [d] \to \forall d \in 𝒫 h d ≼ g [d])$
225	222 223 224	sylc	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall d \in 𝒫 h d ≼ g [d]$
226		elpwi	$⊢ d \in 𝒫 h \to d \subseteq h$
227		resima2	$⊢ d \subseteq h \to ({g ↾}_{h}) [d] = g [d]$
228	226 227	syl	$⊢ d \in 𝒫 h \to ({g ↾}_{h}) [d] = g [d]$
229	228	eqcomd	$⊢ d \in 𝒫 h \to g [d] = ({g ↾}_{h}) [d]$
230	229	breq2d	$⊢ d \in 𝒫 h \to (d ≼ g [d] \leftrightarrow d ≼ ({g ↾}_{h}) [d])$
231	230	ralbiia	$⊢ \forall d \in 𝒫 h d ≼ g [d] \leftrightarrow \forall d \in 𝒫 h d ≼ ({g ↾}_{h}) [d]$
232	225 231	sylib	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall d \in 𝒫 h d ≼ ({g ↾}_{h}) [d]$
233		imaeq1	$⊢ c = {g ↾}_{h} \to c [d] = ({g ↾}_{h}) [d]$
234	233	breq2d	$⊢ c = {g ↾}_{h} \to (d ≼ c [d] \leftrightarrow d ≼ ({g ↾}_{h}) [d])$
235	234	ralbidv	$⊢ c = {g ↾}_{h} \to (\forall d \in 𝒫 h d ≼ c [d] \leftrightarrow \forall d \in 𝒫 h d ≼ ({g ↾}_{h}) [d])$
236		pweq	$⊢ c = {g ↾}_{h} \to 𝒫 c = 𝒫 ({g ↾}_{h})$
237	236	rexeqdv	$⊢ c = {g ↾}_{h} \to (\exists e \in 𝒫 c e : h \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 ({g ↾}_{h}) e : h \underset{1-1}{⟶} V)$
238	235 237	imbi12d	$⊢ c = {g ↾}_{h} \to ((\forall d \in 𝒫 h d ≼ c [d] \to \exists e \in 𝒫 c e : h \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 h d ≼ ({g ↾}_{h}) [d] \to \exists e \in 𝒫 ({g ↾}_{h}) e : h \underset{1-1}{⟶} V))$
239		simpllr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))$
240		psseq1	$⊢ a = h \to (a \subset f \leftrightarrow h \subset f)$
241		xpeq1	$⊢ a = h \to a \times b = h \times b$
242	241	pweqd	$⊢ a = h \to 𝒫 (a \times b) = 𝒫 (h \times b)$
243		pweq	$⊢ a = h \to 𝒫 a = 𝒫 h$
244	243	raleqdv	$⊢ a = h \to (\forall d \in 𝒫 a d ≼ c [d] \leftrightarrow \forall d \in 𝒫 h d ≼ c [d])$
245		f1eq2	$⊢ a = h \to (e : a \underset{1-1}{⟶} V \leftrightarrow e : h \underset{1-1}{⟶} V)$
246	245	rexbidv	$⊢ a = h \to (\exists e \in 𝒫 c e : a \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 c e : h \underset{1-1}{⟶} V)$
247	244 246	imbi12d	$⊢ a = h \to ((\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 h d ≼ c [d] \to \exists e \in 𝒫 c e : h \underset{1-1}{⟶} V))$
248	242 247	raleqbidv	$⊢ a = h \to (\forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow \forall c \in 𝒫 (h \times b) (\forall d \in 𝒫 h d ≼ c [d] \to \exists e \in 𝒫 c e : h \underset{1-1}{⟶} V))$
249	240 248	imbi12d	$⊢ a = h \to ((a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \leftrightarrow (h \subset f \to \forall c \in 𝒫 (h \times b) (\forall d \in 𝒫 h d ≼ c [d] \to \exists e \in 𝒫 c e : h \underset{1-1}{⟶} V)))$
250	249	spvv	$⊢ \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \to (h \subset f \to \forall c \in 𝒫 (h \times b) (\forall d \in 𝒫 h d ≼ c [d] \to \exists e \in 𝒫 c e : h \underset{1-1}{⟶} V))$
251	239 219 250	sylc	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall c \in 𝒫 (h \times b) (\forall d \in 𝒫 h d ≼ c [d] \to \exists e \in 𝒫 c e : h \underset{1-1}{⟶} V)$
252		simplrl	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to g \in 𝒫 (f \times b)$
253		ssres	$⊢ g \subseteq f \times b \to {g ↾}_{h} \subseteq {(f \times b) ↾}_{h}$
254		df-res	$⊢ {(f \times b) ↾}_{h} = (f \times b) \cap (h \times V)$
255		inxp	$⊢ (f \times b) \cap (h \times V) = (f \cap h) \times (b \cap V)$
256		inss2	$⊢ f \cap h \subseteq h$
257		inss1	$⊢ b \cap V \subseteq b$
258		xpss12	$⊢ (f \cap h \subseteq h \land b \cap V \subseteq b) \to (f \cap h) \times (b \cap V) \subseteq h \times b$
259	256 257 258	mp2an	$⊢ (f \cap h) \times (b \cap V) \subseteq h \times b$
260	255 259	eqsstri	$⊢ (f \times b) \cap (h \times V) \subseteq h \times b$
261	254 260	eqsstri	$⊢ {(f \times b) ↾}_{h} \subseteq h \times b$
262	253 261	sstrdi	$⊢ g \subseteq f \times b \to {g ↾}_{h} \subseteq h \times b$
263	94 262	syl	$⊢ g \in 𝒫 (f \times b) \to {g ↾}_{h} \subseteq h \times b$
264	45	resex	$⊢ {g ↾}_{h} \in V$
265	264	elpw	$⊢ {g ↾}_{h} \in 𝒫 (h \times b) \leftrightarrow {g ↾}_{h} \subseteq h \times b$
266	263 265	sylibr	$⊢ g \in 𝒫 (f \times b) \to {g ↾}_{h} \in 𝒫 (h \times b)$
267	252 266	syl	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to {g ↾}_{h} \in 𝒫 (h \times b)$
268	238 251 267	rspcdva	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to (\forall d \in 𝒫 h d ≼ ({g ↾}_{h}) [d] \to \exists e \in 𝒫 ({g ↾}_{h}) e : h \underset{1-1}{⟶} V)$
269	232 268	mpd	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \exists e \in 𝒫 ({g ↾}_{h}) e : h \underset{1-1}{⟶} V$
270		f1eq1	$⊢ e = i \to (e : h \underset{1-1}{⟶} V \leftrightarrow i : h \underset{1-1}{⟶} V)$
271	270	cbvrexvw	$⊢ \exists e \in 𝒫 ({g ↾}_{h}) e : h \underset{1-1}{⟶} V \leftrightarrow \exists i \in 𝒫 ({g ↾}_{h}) i : h \underset{1-1}{⟶} V$
272	269 271	sylib	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \exists i \in 𝒫 ({g ↾}_{h}) i : h \underset{1-1}{⟶} V$
273		id	$⊢ d = h \cup c \to d = h \cup c$
274		imaeq2	$⊢ d = h \cup c \to g [d] = g [h \cup c]$
275	273 274	breq12d	$⊢ d = h \cup c \to (d ≼ g [d] \leftrightarrow (h \cup c) ≼ g [h \cup c])$
276		simprr	$⊢ ((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \to \forall d \in 𝒫 f d ≼ g [d]$
277	276	ad2antrr	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to \forall d \in 𝒫 f d ≼ g [d]$
278	220	ad2antrr	$⊢ ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h]) \to h \subseteq f$
279	278	ad2antlr	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h \subseteq f$
280		elpwi	$⊢ c \in 𝒫 (f ∖ h) \to c \subseteq f ∖ h$
281		difss	$⊢ f ∖ h \subseteq f$
282	280 281	sstrdi	$⊢ c \in 𝒫 (f ∖ h) \to c \subseteq f$
283	282	adantl	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to c \subseteq f$
284	279 283	unssd	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h \cup c \subseteq f$
285	128	elpw2	$⊢ h \cup c \in 𝒫 f \leftrightarrow h \cup c \subseteq f$
286	284 285	sylibr	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h \cup c \in 𝒫 f$
287	275 277 286	rspcdva	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to (h \cup c) ≼ g [h \cup c]$
288		imaundi	$⊢ g [h \cup c] = g [h] \cup g [c]$
289		undif2	$⊢ g [h] \cup (g [c] ∖ g [h]) = g [h] \cup g [c]$
290	288 289	eqtr4i	$⊢ g [h \cup c] = g [h] \cup (g [c] ∖ g [h])$
291	287 290	breqtrdi	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to (h \cup c) ≼ (g [h] \cup (g [c] ∖ g [h]))$
292		simp-4l	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to f \in Fin$
293	292 279	ssfid	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h \in Fin$
294		id	$⊢ d = h \to d = h$
295		imaeq2	$⊢ d = h \to g [d] = g [h]$
296	294 295	breq12d	$⊢ d = h \to (d ≼ g [d] \leftrightarrow h ≼ g [h])$
297		vex	$⊢ h \in V$
298	297	elpw	$⊢ h \in 𝒫 f \leftrightarrow h \subseteq f$
299	279 298	sylibr	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h \in 𝒫 f$
300	296 277 299	rspcdva	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h ≼ g [h]$
301		simplrr	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to \neg h ≺ g [h]$
302		bren2	$⊢ h \approx g [h] \leftrightarrow (h ≼ g [h] \land \neg h ≺ g [h])$
303	300 301 302	sylanbrc	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h \approx g [h]$
304	303	ensymd	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to g [h] \approx h$
305		incom	$⊢ h \cap c = c \cap h$
306		ssdifin0	$⊢ c \subseteq f ∖ h \to c \cap h = \emptyset$
307	305 306	syl5eq	$⊢ c \subseteq f ∖ h \to h \cap c = \emptyset$
308	280 307	syl	$⊢ c \in 𝒫 (f ∖ h) \to h \cap c = \emptyset$
309	308	adantl	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to h \cap c = \emptyset$
310		disjdif	$⊢ g [h] \cap (g [c] ∖ g [h]) = \emptyset$
311	310	a1i	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to g [h] \cap (g [c] ∖ g [h]) = \emptyset$
312		domunfican	$⊢ ((h \in Fin \land g [h] \approx h) \land (h \cap c = \emptyset \land g [h] \cap (g [c] ∖ g [h]) = \emptyset)) \to ((h \cup c) ≼ (g [h] \cup (g [c] ∖ g [h])) \leftrightarrow c ≼ (g [c] ∖ g [h]))$
313	293 304 309 311 312	syl22anc	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to ((h \cup c) ≼ (g [h] \cup (g [c] ∖ g [h])) \leftrightarrow c ≼ (g [c] ∖ g [h]))$
314	291 313	mpbid	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to c ≼ (g [c] ∖ g [h])$
315	101	difeq1d	$⊢ g \in 𝒫 (f \times b) \to (g [c] \cap b) ∖ g [h] = g [c] ∖ g [h]$
316	315	ad2antrl	$⊢ ((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \to (g [c] \cap b) ∖ g [h] = g [c] ∖ g [h]$
317	316	ad2antrr	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to (g [c] \cap b) ∖ g [h] = g [c] ∖ g [h]$
318	314 317	breqtrrd	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to c ≼ ((g [c] \cap b) ∖ g [h])$
319		df-ss	$⊢ c \subseteq f ∖ h \leftrightarrow c \cap (f ∖ h) = c$
320	280 319	sylib	$⊢ c \in 𝒫 (f ∖ h) \to c \cap (f ∖ h) = c$
321	320	imaeq2d	$⊢ c \in 𝒫 (f ∖ h) \to g [c \cap (f ∖ h)] = g [c]$
322	321	ineq1d	$⊢ c \in 𝒫 (f ∖ h) \to g [c \cap (f ∖ h)] \cap (b ∖ g [h]) = g [c] \cap (b ∖ g [h])$
323		indif2	$⊢ g [c] \cap (b ∖ g [h]) = (g [c] \cap b) ∖ g [h]$
324	322 323	eqtrdi	$⊢ c \in 𝒫 (f ∖ h) \to g [c \cap (f ∖ h)] \cap (b ∖ g [h]) = (g [c] \cap b) ∖ g [h]$
325	324	adantl	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to g [c \cap (f ∖ h)] \cap (b ∖ g [h]) = (g [c] \cap b) ∖ g [h]$
326	318 325	breqtrrd	$⊢ ((((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \land c \in 𝒫 (f ∖ h)) \to c ≼ (g [c \cap (f ∖ h)] \cap (b ∖ g [h]))$
327	326	ralrimiva	$⊢ (((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall c \in 𝒫 (f ∖ h) c ≼ (g [c \cap (f ∖ h)] \cap (b ∖ g [h]))$
328		imainrect	$⊢ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [c] = g [c \cap (f ∖ h)] \cap (b ∖ g [h])$
329		imaeq2	$⊢ c = d \to (g \cap ((f ∖ h) \times (b ∖ g [h]))) [c] = (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d]$
330	328 329	eqtr3id	$⊢ c = d \to g [c \cap (f ∖ h)] \cap (b ∖ g [h]) = (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d]$
331	109 330	breq12d	$⊢ c = d \to (c ≼ (g [c \cap (f ∖ h)] \cap (b ∖ g [h])) \leftrightarrow d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d])$
332	331	cbvralvw	$⊢ \forall c \in 𝒫 (f ∖ h) c ≼ (g [c \cap (f ∖ h)] \cap (b ∖ g [h])) \leftrightarrow \forall d \in 𝒫 (f ∖ h) d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d]$
333	327 332	sylib	$⊢ (((f \in Fin \land b \in Fin) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall d \in 𝒫 (f ∖ h) d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d]$
334	333	adantllr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall d \in 𝒫 (f ∖ h) d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d]$
335		inss2	$⊢ g \cap ((f ∖ h) \times (b ∖ g [h])) \subseteq (f ∖ h) \times (b ∖ g [h])$
336		difss	$⊢ b ∖ g [h] \subseteq b$
337		xpss2	$⊢ b ∖ g [h] \subseteq b \to (f ∖ h) \times (b ∖ g [h]) \subseteq (f ∖ h) \times b$
338	336 337	ax-mp	$⊢ (f ∖ h) \times (b ∖ g [h]) \subseteq (f ∖ h) \times b$
339	335 338	sstri	$⊢ g \cap ((f ∖ h) \times (b ∖ g [h])) \subseteq (f ∖ h) \times b$
340	45	inex1	$⊢ g \cap ((f ∖ h) \times (b ∖ g [h])) \in V$
341	340	elpw	$⊢ g \cap ((f ∖ h) \times (b ∖ g [h])) \in 𝒫 ((f ∖ h) \times b) \leftrightarrow g \cap ((f ∖ h) \times (b ∖ g [h])) \subseteq (f ∖ h) \times b$
342	339 341	mpbir	$⊢ g \cap ((f ∖ h) \times (b ∖ g [h])) \in 𝒫 ((f ∖ h) \times b)$
343		incom	$⊢ f \cap h = h \cap f$
344		df-ss	$⊢ h \subseteq f \leftrightarrow h \cap f = h$
345	220 344	sylib	$⊢ h \subset f \to h \cap f = h$
346	343 345	syl5eq	$⊢ h \subset f \to f \cap h = h$
347	346	neeq1d	$⊢ h \subset f \to (f \cap h \neq \emptyset \leftrightarrow h \neq \emptyset)$
348	347	biimpar	$⊢ (h \subset f \land h \neq \emptyset) \to f \cap h \neq \emptyset$
349		disj4	$⊢ f \cap h = \emptyset \leftrightarrow \neg f ∖ h \subset f$
350	349	bicomi	$⊢ \neg f ∖ h \subset f \leftrightarrow f \cap h = \emptyset$
351	350	necon1abii	$⊢ f \cap h \neq \emptyset \leftrightarrow f ∖ h \subset f$
352	348 351	sylib	$⊢ (h \subset f \land h \neq \emptyset) \to f ∖ h \subset f$
353	352	ad2antrl	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to f ∖ h \subset f$
354	128	difexi	$⊢ f ∖ h \in V$
355		psseq1	$⊢ a = f ∖ h \to (a \subset f \leftrightarrow f ∖ h \subset f)$
356		xpeq1	$⊢ a = f ∖ h \to a \times b = (f ∖ h) \times b$
357	356	pweqd	$⊢ a = f ∖ h \to 𝒫 (a \times b) = 𝒫 ((f ∖ h) \times b)$
358		pweq	$⊢ a = f ∖ h \to 𝒫 a = 𝒫 (f ∖ h)$
359	358	raleqdv	$⊢ a = f ∖ h \to (\forall d \in 𝒫 a d ≼ c [d] \leftrightarrow \forall d \in 𝒫 (f ∖ h) d ≼ c [d])$
360		f1eq2	$⊢ a = f ∖ h \to (e : a \underset{1-1}{⟶} V \leftrightarrow e : f ∖ h \underset{1-1}{⟶} V)$
361	360	rexbidv	$⊢ a = f ∖ h \to (\exists e \in 𝒫 c e : a \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V)$
362	359 361	imbi12d	$⊢ a = f ∖ h \to ((\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V))$
363	357 362	raleqbidv	$⊢ a = f ∖ h \to (\forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V) \leftrightarrow \forall c \in 𝒫 ((f ∖ h) \times b) (\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V))$
364	355 363	imbi12d	$⊢ a = f ∖ h \to ((a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \leftrightarrow (f ∖ h \subset f \to \forall c \in 𝒫 ((f ∖ h) \times b) (\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V)))$
365	354 364	spcv	$⊢ \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \to (f ∖ h \subset f \to \forall c \in 𝒫 ((f ∖ h) \times b) (\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V))$
366	239 353 365	sylc	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \forall c \in 𝒫 ((f ∖ h) \times b) (\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V)$
367		imaeq1	$⊢ c = g \cap ((f ∖ h) \times (b ∖ g [h])) \to c [d] = (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d]$
368	367	breq2d	$⊢ c = g \cap ((f ∖ h) \times (b ∖ g [h])) \to (d ≼ c [d] \leftrightarrow d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d])$
369	368	ralbidv	$⊢ c = g \cap ((f ∖ h) \times (b ∖ g [h])) \to (\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \leftrightarrow \forall d \in 𝒫 (f ∖ h) d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d])$
370		pweq	$⊢ c = g \cap ((f ∖ h) \times (b ∖ g [h])) \to 𝒫 c = 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h])))$
371	370	rexeqdv	$⊢ c = g \cap ((f ∖ h) \times (b ∖ g [h])) \to (\exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) e : f ∖ h \underset{1-1}{⟶} V)$
372	369 371	imbi12d	$⊢ c = g \cap ((f ∖ h) \times (b ∖ g [h])) \to ((\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 (f ∖ h) d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d] \to \exists e \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) e : f ∖ h \underset{1-1}{⟶} V))$
373	372	rspcva	$⊢ (g \cap ((f ∖ h) \times (b ∖ g [h])) \in 𝒫 ((f ∖ h) \times b) \land \forall c \in 𝒫 ((f ∖ h) \times b) (\forall d \in 𝒫 (f ∖ h) d ≼ c [d] \to \exists e \in 𝒫 c e : f ∖ h \underset{1-1}{⟶} V)) \to (\forall d \in 𝒫 (f ∖ h) d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d] \to \exists e \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) e : f ∖ h \underset{1-1}{⟶} V)$
374	342 366 373	sylancr	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to (\forall d \in 𝒫 (f ∖ h) d ≼ (g \cap ((f ∖ h) \times (b ∖ g [h]))) [d] \to \exists e \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) e : f ∖ h \underset{1-1}{⟶} V)$
375	334 374	mpd	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \exists e \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) e : f ∖ h \underset{1-1}{⟶} V$
376		f1eq1	$⊢ e = j \to (e : f ∖ h \underset{1-1}{⟶} V \leftrightarrow j : f ∖ h \underset{1-1}{⟶} V)$
377	376	cbvrexvw	$⊢ \exists e \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) e : f ∖ h \underset{1-1}{⟶} V \leftrightarrow \exists j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) j : f ∖ h \underset{1-1}{⟶} V$
378	375 377	sylib	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \exists j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) j : f ∖ h \underset{1-1}{⟶} V$
379		elpwi	$⊢ i \in 𝒫 ({g ↾}_{h}) \to i \subseteq {g ↾}_{h}$
380		resss	$⊢ {g ↾}_{h} \subseteq g$
381	379 380	sstrdi	$⊢ i \in 𝒫 ({g ↾}_{h}) \to i \subseteq g$
382	381	adantr	$⊢ (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V) \to i \subseteq g$
383	382	ad2antlr	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to i \subseteq g$
384		elpwi	$⊢ j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \to j \subseteq g \cap ((f ∖ h) \times (b ∖ g [h]))$
385		inss1	$⊢ g \cap ((f ∖ h) \times (b ∖ g [h])) \subseteq g$
386	384 385	sstrdi	$⊢ j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \to j \subseteq g$
387	386	ad2antrl	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to j \subseteq g$
388	383 387	unssd	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to i \cup j \subseteq g$
389	45	elpw2	$⊢ i \cup j \in 𝒫 g \leftrightarrow i \cup j \subseteq g$
390	388 389	sylibr	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to i \cup j \in 𝒫 g$
391		f1f1orn	$⊢ i : h \underset{1-1}{⟶} V \to i : h \underset{1-1 onto}{⟶} ran i$
392	391	adantl	$⊢ (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V) \to i : h \underset{1-1 onto}{⟶} ran i$
393	392	ad2antlr	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to i : h \underset{1-1 onto}{⟶} ran i$
394		f1f1orn	$⊢ j : f ∖ h \underset{1-1}{⟶} V \to j : f ∖ h \underset{1-1 onto}{⟶} ran j$
395	394	ad2antll	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to j : f ∖ h \underset{1-1 onto}{⟶} ran j$
396		disjdif	$⊢ h \cap (f ∖ h) = \emptyset$
397	396	a1i	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to h \cap (f ∖ h) = \emptyset$
398		rnss	$⊢ i \subseteq {g ↾}_{h} \to ran i \subseteq ran ({g ↾}_{h})$
399	379 398	syl	$⊢ i \in 𝒫 ({g ↾}_{h}) \to ran i \subseteq ran ({g ↾}_{h})$
400		df-ima	$⊢ g [h] = ran ({g ↾}_{h})$
401	399 400	sseqtrrdi	$⊢ i \in 𝒫 ({g ↾}_{h}) \to ran i \subseteq g [h]$
402	401	adantr	$⊢ (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V) \to ran i \subseteq g [h]$
403	402	ad2antlr	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to ran i \subseteq g [h]$
404		incom	$⊢ g [h] \cap ran j = ran j \cap g [h]$
405	384 335	sstrdi	$⊢ j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \to j \subseteq (f ∖ h) \times (b ∖ g [h])$
406		rnss	$⊢ j \subseteq (f ∖ h) \times (b ∖ g [h]) \to ran j \subseteq ran ((f ∖ h) \times (b ∖ g [h]))$
407	405 406	syl	$⊢ j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \to ran j \subseteq ran ((f ∖ h) \times (b ∖ g [h]))$
408		rnxpss	$⊢ ran ((f ∖ h) \times (b ∖ g [h])) \subseteq b ∖ g [h]$
409	407 408	sstrdi	$⊢ j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \to ran j \subseteq b ∖ g [h]$
410	409	ad2antrl	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to ran j \subseteq b ∖ g [h]$
411		disjdifr	$⊢ (b ∖ g [h]) \cap g [h] = \emptyset$
412		ssdisj	$⊢ (ran j \subseteq b ∖ g [h] \land (b ∖ g [h]) \cap g [h] = \emptyset) \to ran j \cap g [h] = \emptyset$
413	410 411 412	sylancl	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to ran j \cap g [h] = \emptyset$
414	404 413	syl5eq	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to g [h] \cap ran j = \emptyset$
415		ssdisj	$⊢ (ran i \subseteq g [h] \land g [h] \cap ran j = \emptyset) \to ran i \cap ran j = \emptyset$
416	403 414 415	syl2anc	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to ran i \cap ran j = \emptyset$
417		f1oun	$⊢ ((i : h \underset{1-1 onto}{⟶} ran i \land j : f ∖ h \underset{1-1 onto}{⟶} ran j) \land (h \cap (f ∖ h) = \emptyset \land ran i \cap ran j = \emptyset)) \to (i \cup j) : h \cup (f ∖ h) \underset{1-1 onto}{⟶} ran i \cup ran j$
418	393 395 397 416 417	syl22anc	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to (i \cup j) : h \cup (f ∖ h) \underset{1-1 onto}{⟶} ran i \cup ran j$
419		undif	$⊢ h \subseteq f \leftrightarrow h \cup (f ∖ h) = f$
420	419	biimpi	$⊢ h \subseteq f \to h \cup (f ∖ h) = f$
421	420	adantl	$⊢ (g \in 𝒫 (f \times b) \land h \subseteq f) \to h \cup (f ∖ h) = f$
422	421	ad2antrr	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to h \cup (f ∖ h) = f$
423	422	f1oeq2d	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to ((i \cup j) : h \cup (f ∖ h) \underset{1-1 onto}{⟶} ran i \cup ran j \leftrightarrow (i \cup j) : f \underset{1-1 onto}{⟶} ran i \cup ran j)$
424	418 423	mpbid	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to (i \cup j) : f \underset{1-1 onto}{⟶} ran i \cup ran j$
425		f1of1	$⊢ (i \cup j) : f \underset{1-1 onto}{⟶} ran i \cup ran j \to (i \cup j) : f \underset{1-1}{⟶} ran i \cup ran j$
426	424 425	syl	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to (i \cup j) : f \underset{1-1}{⟶} ran i \cup ran j$
427		ssv	$⊢ ran i \cup ran j \subseteq V$
428		f1ss	$⊢ ((i \cup j) : f \underset{1-1}{⟶} ran i \cup ran j \land ran i \cup ran j \subseteq V) \to (i \cup j) : f \underset{1-1}{⟶} V$
429	426 427 428	sylancl	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to (i \cup j) : f \underset{1-1}{⟶} V$
430		f1eq1	$⊢ e = i \cup j \to (e : f \underset{1-1}{⟶} V \leftrightarrow (i \cup j) : f \underset{1-1}{⟶} V)$
431	430	rspcev	$⊢ (i \cup j \in 𝒫 g \land (i \cup j) : f \underset{1-1}{⟶} V) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
432	390 429 431	syl2anc	$⊢ (((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \land (j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) \land j : f ∖ h \underset{1-1}{⟶} V)) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
433	432	rexlimdvaa	$⊢ ((g \in 𝒫 (f \times b) \land h \subseteq f) \land (i \in 𝒫 ({g ↾}_{h}) \land i : h \underset{1-1}{⟶} V)) \to (\exists j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) j : f ∖ h \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
434	433	rexlimdvaa	$⊢ (g \in 𝒫 (f \times b) \land h \subseteq f) \to (\exists i \in 𝒫 ({g ↾}_{h}) i : h \underset{1-1}{⟶} V \to (\exists j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) j : f ∖ h \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V))$
435	252 221 434	syl2anc	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to (\exists i \in 𝒫 ({g ↾}_{h}) i : h \underset{1-1}{⟶} V \to (\exists j \in 𝒫 (g \cap ((f ∖ h) \times (b ∖ g [h]))) j : f ∖ h \underset{1-1}{⟶} V \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V))$
436	272 378 435	mp2d	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
437	436	ex	$⊢ (((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \to (((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h]) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
438	437	exlimdv	$⊢ (((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \to (\exists h ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h]) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
439	438	imp	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \exists h ((h \subset f \land h \neq \emptyset) \land \neg h ≺ g [h])) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
440	218 439	sylan2br	$⊢ ((((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \land \neg \forall h ((h \subset f \land h \neq \emptyset) \to h ≺ g [h])) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
441	217 440	pm2.61dan	$⊢ (((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \land (g \in 𝒫 (f \times b) \land \forall d \in 𝒫 f d ≼ g [d])) \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V$
442	441	exp32	$⊢ ((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \to (g \in 𝒫 (f \times b) \to (\forall d \in 𝒫 f d ≼ g [d] \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V))$
443	442	ralrimiv	$⊢ ((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \to \forall g \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ g [d] \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V)$
444		imaeq1	$⊢ g = c \to g [d] = c [d]$
445	444	breq2d	$⊢ g = c \to (d ≼ g [d] \leftrightarrow d ≼ c [d])$
446	445	ralbidv	$⊢ g = c \to (\forall d \in 𝒫 f d ≼ g [d] \leftrightarrow \forall d \in 𝒫 f d ≼ c [d])$
447		pweq	$⊢ g = c \to 𝒫 g = 𝒫 c$
448	447	rexeqdv	$⊢ g = c \to (\exists e \in 𝒫 g e : f \underset{1-1}{⟶} V \leftrightarrow \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)$
449	446 448	imbi12d	$⊢ g = c \to ((\forall d \in 𝒫 f d ≼ g [d] \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V))$
450	449	cbvralvw	$⊢ \forall g \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ g [d] \to \exists e \in 𝒫 g e : f \underset{1-1}{⟶} V) \leftrightarrow \forall c \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)$
451	443 450	sylib	$⊢ ((f \in Fin \land b \in Fin) \land \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \to \forall c \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)$
452	451	exp31	$⊢ f \in Fin \to (b \in Fin \to (\forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V)) \to \forall c \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)))$
453	452	a2d	$⊢ f \in Fin \to ((b \in Fin \to \forall a (a \subset f \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \to (b \in Fin \to \forall c \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)))$
454	22 453	syl5bi	$⊢ f \in Fin \to (\forall a (a \subset f \to (b \in Fin \to \forall c \in 𝒫 (a \times b) (\forall d \in 𝒫 a d ≼ c [d] \to \exists e \in 𝒫 c e : a \underset{1-1}{⟶} V))) \to (b \in Fin \to \forall c \in 𝒫 (f \times b) (\forall d \in 𝒫 f d ≼ c [d] \to \exists e \in 𝒫 c e : f \underset{1-1}{⟶} V)))$
455	9 18 454	findcard3	$⊢ A \in Fin \to (b \in Fin \to \forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists e \in 𝒫 c e : A \underset{1-1}{⟶} V))$

Metamath Proof Explorer

Theorem marypha1lem

Proof