Theorem marypha1lem 8900

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

Assertion

Ref	Expression
marypha1lem	⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

Distinct variable group:   𝐴,𝑏,𝑐,𝑑,𝑒

Proof of Theorem marypha1lem

Dummy variables 𝑎 𝑓 𝑔 ℎ 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpeq1 5572	. . . . 5 ⊢ (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
2	1	pweqd 4561	. . . 4 ⊢ (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3		pweq 4558	. . . . . 6 ⊢ (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
4	3	raleqdv 3418	. . . . 5 ⊢ (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
5		f1eq2 6574	. . . . . 6 ⊢ (𝑎 = 𝑓 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝑓–1-1→V))
6	5	rexbidv 3300	. . . . 5 ⊢ (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
7	4, 6	imbi12d 347	. . . 4 ⊢ (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
8	2, 7	raleqbidv 3404	. . 3 ⊢ (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
9	8	imbi2d 343	. 2 ⊢ (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
10		xpeq1 5572	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
11	10	pweqd 4561	. . . 4 ⊢ (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12		pweq 4558	. . . . . 6 ⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
13	12	raleqdv 3418	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑)))
14		f1eq2 6574	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝐴–1-1→V))
15	14	rexbidv 3300	. . . . 5 ⊢ (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))
16	13, 15	imbi12d 347	. . . 4 ⊢ (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
17	11, 16	raleqbidv 3404	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
18	17	imbi2d 343	. 2 ⊢ (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))))
19		bi2.04 391	. . . . 5 ⊢ ((𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
20	19	albii 1819	. . . 4 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
21		19.21v 1939	. . . 4 ⊢ (∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
22	20, 21	bitri 277	. . 3 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
23		0elpw 5259	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑔
24		f10 6650	. . . . . . . . . . . . 13 ⊢ ∅:∅–1-1→V
25		f1eq1 6573	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
26	25	rspcev 3626	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
27	23, 24, 26	mp2an 690	. . . . . . . . . . . 12 ⊢ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28		f1eq2 6574	. . . . . . . . . . . . 13 ⊢ (𝑓 = ∅ → (𝑒:𝑓–1-1→V ↔ 𝑒:∅–1-1→V))
29	28	rexbidv 3300	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
30	27, 29	mpbiri 260	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
32		n0 4313	. . . . . . . . . . 11 ⊢ (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖 ∈ 𝑓)
33		snelpwi 5340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ∈ 𝒫 𝑓)
34		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → 𝑑 = {𝑖})
35		imaeq2 5928	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → (𝑔 “ 𝑑) = (𝑔 “ {𝑖}))
36	34, 35	breq12d 5082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑖} → (𝑑 ≼ (𝑔 “ 𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
37	36	rspcva 3624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38		vex 3500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑖 ∈ V
39	38	snnz 4714	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑖} ≠ ∅
40		snex 5335	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑖} ∈ V
41	40	0sdom 8651	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
42	39, 41	mpbir 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ≺ {𝑖}
43		sdomdomtr 8653	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
44	42, 43	mpan 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45		vex 3500	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
46	45	imaex 7624	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ {𝑖}) ∈ V
47	46	0sdom 8651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
48	44, 47	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
49	37, 48	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
50	49	expcom 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
51	33, 50	syl5 34	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
52	51	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
53	52	ad2antlr 725	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
54	53	impr 457	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
55		n0 4313	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
56	54, 55	sylib 220	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
57	45	imaex 7624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ∈ V
58	57	difexi 5235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ∖ {𝑗}) ∈ V
59	58	0dom 8650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})
60		breq1 5072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = ∅ → (𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
61	59, 60	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
63		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
64		elpwi 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
65	64	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
66		difsnpss 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
67	66	biimpi 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 ∈ 𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
68	67	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
69	65, 68	sspsstrd 4088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊊ 𝑓)
70		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
71	69, 70	jca 514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅))
72		psseq1 4067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ⊊ 𝑓 ↔ 𝑐 ⊊ 𝑓))
73		neeq1 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ≠ ∅ ↔ 𝑐 ≠ ∅))
74	72, 73	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ↔ (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅)))
75		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → ℎ = 𝑐)
76		imaeq2 5928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (𝑔 “ ℎ) = (𝑔 “ 𝑐))
77	75, 76	breq12d 5082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → (ℎ ≺ (𝑔 “ ℎ) ↔ 𝑐 ≺ (𝑔 “ 𝑐)))
78	74, 77	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ℎ = 𝑐 → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ↔ ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐))))
79	78	spvv 2002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) → ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐)))
80	63, 71, 79	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔 “ 𝑐))
81		domdifsn 8603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ≺ (𝑔 “ 𝑐) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
83	82	expr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
84	62, 83	pm2.61dne 3106	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
85	84	adantlrr 719	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
86	85	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
87		df-ss 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
88	64, 87	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
89	88	imaeq2d 5932	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔 “ 𝑐))
90	89	ineq1d 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
91	90	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
92		indif2 4250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗})
93		imassrn 5943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ⊆ ran 𝑔
94		elpwi 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
95		rnss 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
96		rnxpss 6032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ran (𝑓 × 𝑏) ⊆ 𝑏
97	95, 96	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
98	94, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
99	93, 98	sstrid 3981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 “ 𝑐) ⊆ 𝑏)
100		df-ss 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ⊆ 𝑏 ↔ ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
101	99, 100	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
102	101	difeq1d 4101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
103	102	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
104	92, 103	syl5eq 2871	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
105	104	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
106	91, 105	eqtrd 2859	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
107	86, 106	breqtrrd 5097	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
108	107	ralrimiva 3185	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
109		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → 𝑐 = 𝑑)
110		imainrect 6041	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
111		imaeq2 5928	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
112	110, 111	syl5eqr 2873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
113	109, 112	breq12d 5082	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
114	113	cbvralvw 3452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115	108, 114	sylib 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
116	115	adantllr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117		inss2 4209	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
118		difss 4111	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∖ {𝑗}) ⊆ 𝑏
119		xpss2 5578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
121	117, 120	sstri 3979	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
122	45	inex1 5224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
123	122	elpw 4546	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
124	121, 123	mpbir 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
125		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
126	67	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
127	126	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
128		vex 3500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑓 ∈ V
129	128	difexi 5235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∖ {𝑖}) ∈ V
130		psseq1 4067	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
131		xpeq1 5572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
132	131	pweqd 4561	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
133		pweq 4558	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
134	133	raleqdv 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑)))
135		f1eq2 6574	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
136	135	rexbidv 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
137	134, 136	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
138	132, 137	raleqbidv 3404	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
139	130, 138	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
140	129, 139	spcv 3609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141	125, 127, 140	sylc 65	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
142		imaeq1 5927	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
143	142	breq2d 5081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
144	143	ralbidv 3200	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
145		pweq 4558	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
146	145	rexeqdv 3419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
147	144, 146	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
148	147	rspcva 3624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
149	124, 141, 148	sylancr 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
150	116, 149	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)
151		f1eq1 6573	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
152	151	cbvrexvw 3453	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
153	150, 152	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
154		vex 3500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑗 ∈ V
155	38, 154	elimasn 5957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
156	155	biimpi 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
157	156	snssd 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
158	157	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
159		elpwi 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
160		inss1 4208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
161	159, 160	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ 𝑔)
162	161	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘 ⊆ 𝑔)
163	158, 162	unssd 4165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
164	45	elpw2 5251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
165	163, 164	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
166	165	ad2ant2lr 746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
167	38, 154	f1osn 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
169		f1f1orn 6629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
170	169	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
171		disjdif 4424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
173		incom 4181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
174	159, 117	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
175		rnss 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
176		rnxpss 6032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
177	175, 176	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
178	174, 177	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
179		incom 4181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝑏 ∖ {𝑗}))
180		disjdif 4424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({𝑗} ∩ (𝑏 ∖ {𝑗})) = ∅
181	179, 180	eqtri 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
182		ssdisj 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
183	178, 181, 182	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
184	173, 183	syl5eq 2871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
185	184	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
186		f1oun 6637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
187	168, 170, 172, 185, 186	syl22anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
188	187	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
189		snssi 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ⊆ 𝑓)
190	189	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
191		undif 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
192	190, 191	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
193	192	f1oeq2d 6614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
194	193	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
195	188, 194	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘))
196		f1of1 6617	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘))
197		ssv 3994	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑗} ∪ ran 𝑘) ⊆ V
198		f1ss 6583	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
199	196, 197, 198	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
200	195, 199	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
201		f1eq1 6573	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓–1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V))
202	201	rspcev 3626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
203	166, 200, 202	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
204	203	rexlimdvaa 3288	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
205	204	ex 415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
206	205	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
207	206	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
208	207	impr 457	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
209	208	adantllr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
210	153, 209	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
211	210	expr 459	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
212	211	expd 418	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
213	212	impr 457	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
214	213	exlimdv 1933	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
215	56, 214	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
216	215	expr 459	. . . . . . . . . . . 12 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
217	216	exlimdv 1933	. . . . . . . . . . 11 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
218	32, 217	syl5bi 244	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
219	31, 218	pm2.61dne 3106	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
220		exanali 1858	. . . . . . . . . 10 ⊢ (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) ↔ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
221		simprll 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊊ 𝑓)
222		pssss 4075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ⊊ 𝑓 → ℎ ⊆ 𝑓)
223	221, 222	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊆ 𝑓)
224	223	sspwd 4557	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝒫 ℎ ⊆ 𝒫 𝑓)
225		simplrr 776	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
226		ssralv 4036	. . . . . . . . . . . . . . . . . 18 ⊢ (𝒫 ℎ ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑)))
227	224, 225, 226	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑))
228		elpwi 4551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ 𝒫 ℎ → 𝑑 ⊆ ℎ)
229		resima2 5891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
230	228, 229	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
231	230	eqcomd 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑔 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
232	231	breq2d 5081	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
233	232	ralbiia 3167	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
234	227, 233	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
235		imaeq1 5927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑐 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
236	235	breq2d 5081	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
237	236	ralbidv 3200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
238		pweq 4558	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → 𝒫 𝑐 = 𝒫 (𝑔 ↾ ℎ))
239	238	rexeqdv 3419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
240	237, 239	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑔 ↾ ℎ) → ((∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)))
241		simpllr 774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
242		psseq1 4067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (𝑎 ⊊ 𝑓 ↔ ℎ ⊊ 𝑓))
243		xpeq1 5572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (𝑎 × 𝑏) = (ℎ × 𝑏))
244	243	pweqd 4561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → 𝒫 (𝑎 × 𝑏) = 𝒫 (ℎ × 𝑏))
245		pweq 4558	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → 𝒫 𝑎 = 𝒫 ℎ)
246	245	raleqdv 3418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑)))
247		f1eq2 6574	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → (𝑒:𝑎–1-1→V ↔ 𝑒:ℎ–1-1→V))
248	247	rexbidv 3300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
249	246, 248	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
250	244, 249	raleqbidv 3404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
251	242, 250	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ℎ → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))))
252	251	spvv 2002	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
253	241, 221, 252	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
254		simplrl 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
255		ssres 5883	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ ((𝑓 × 𝑏) ↾ ℎ))
256		df-res 5570	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ↾ ℎ) = ((𝑓 × 𝑏) ∩ (ℎ × V))
257		inxp 5706	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) = ((𝑓 ∩ ℎ) × (𝑏 ∩ V))
258		inss2 4209	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∩ ℎ) ⊆ ℎ
259		inss1 4208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∩ V) ⊆ 𝑏
260		xpss12 5573	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓 ∩ ℎ) ⊆ ℎ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏))
261	258, 259, 260	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏)
262	257, 261	eqsstri 4004	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) ⊆ (ℎ × 𝑏)
263	256, 262	eqsstri 4004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 × 𝑏) ↾ ℎ) ⊆ (ℎ × 𝑏)
264	255, 263	sstrdi 3982	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
265	94, 264	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
266	45	resex 5902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ↾ ℎ) ∈ V
267	266	elpw 4546	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏) ↔ (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
268	265, 267	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
269	254, 268	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
270	240, 253, 269	rspcdva 3628	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
271	234, 270	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)
272		f1eq1 6573	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑖 → (𝑒:ℎ–1-1→V ↔ 𝑖:ℎ–1-1→V))
273	272	cbvrexvw 3453	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
274	271, 273	sylib 220	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
275		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → 𝑑 = (ℎ ∪ 𝑐))
276		imaeq2 5928	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑔 “ 𝑑) = (𝑔 “ (ℎ ∪ 𝑐)))
277	275, 276	breq12d 5082	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑑 ≼ (𝑔 “ 𝑑) ↔ (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐))))
278		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
279	278	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
280	222	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ℎ ⊆ 𝑓)
281	280	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ⊆ 𝑓)
282		elpwi 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ (𝑓 ∖ ℎ))
283		difss 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∖ ℎ) ⊆ 𝑓
284	282, 283	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ 𝑓)
285	284	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ⊆ 𝑓)
286	281, 285	unssd 4165	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ⊆ 𝑓)
287	128	elpw2 5251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∪ 𝑐) ∈ 𝒫 𝑓 ↔ (ℎ ∪ 𝑐) ⊆ 𝑓)
288	286, 287	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ∈ 𝒫 𝑓)
289	277, 279, 288	rspcdva 3628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐)))
290		imaundi 6011	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
291		undif2 4428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
292	290, 291	eqtr4i 2850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
293	289, 292	breqtrdi 5110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
294		simp-4l 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑓 ∈ Fin)
295	294, 281	ssfid 8744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ Fin)
296		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → 𝑑 = ℎ)
297		imaeq2 5928	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → (𝑔 “ 𝑑) = (𝑔 “ ℎ))
298	296, 297	breq12d 5082	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ ℎ ≼ (𝑔 “ ℎ)))
299		vex 3500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℎ ∈ V
300	299	elpw 4546	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ ∈ 𝒫 𝑓 ↔ ℎ ⊆ 𝑓)
301	281, 300	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ 𝒫 𝑓)
302	298, 279, 301	rspcdva 3628	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≼ (𝑔 “ ℎ))
303		simplrr 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ¬ ℎ ≺ (𝑔 “ ℎ))
304		bren2 8543	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ≈ (𝑔 “ ℎ) ↔ (ℎ ≼ (𝑔 “ ℎ) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)))
305	302, 303, 304	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≈ (𝑔 “ ℎ))
306	305	ensymd 8563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (𝑔 “ ℎ) ≈ ℎ)
307		incom 4181	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∩ 𝑐) = (𝑐 ∩ ℎ)
308		ssdifin0 4434	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (𝑐 ∩ ℎ) = ∅)
309	307, 308	syl5eq 2871	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
310	282, 309	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
311	310	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∩ 𝑐) = ∅)
312		disjdif 4424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅
313	312	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)
314		domunfican 8794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ ∈ Fin ∧ (𝑔 “ ℎ) ≈ ℎ) ∧ ((ℎ ∩ 𝑐) = ∅ ∧ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
315	295, 306, 311, 313, 314	syl22anc 836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
316	293, 315	mpbid 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
317	101	difeq1d 4101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
318	317	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
319	318	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
320	316, 319	breqtrrd 5097	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
321		df-ss 3955	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) ↔ (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
322	282, 321	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
323	322	imaeq2d 5932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) = (𝑔 “ 𝑐))
324	323	ineq1d 4191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
325		indif2 4250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ))
326	324, 325	syl6eq 2875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
327	326	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
328	320, 327	breqtrrd 5097	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
329	328	ralrimiva 3185	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
330		imainrect 6041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
331		imaeq2 5928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
332	330, 331	syl5eqr 2873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
333	109, 332	breq12d 5082	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
334	333	cbvralvw 3452	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
335	329, 334	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
336	335	adantllr 717	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
337		inss2 4209	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))
338		difss 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏
339		xpss2 5578	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏 → ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
340	338, 339	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
341	337, 340	sstri 3979	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
342	45	inex1 5224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ V
343	342	elpw 4546	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
344	341, 343	mpbir 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)
345		incom 4181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∩ ℎ) = (ℎ ∩ 𝑓)
346		df-ss 3955	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∩ 𝑓) = ℎ)
347	222, 346	sylib 220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ⊊ 𝑓 → (ℎ ∩ 𝑓) = ℎ)
348	345, 347	syl5eq 2871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ⊊ 𝑓 → (𝑓 ∩ ℎ) = ℎ)
349	348	neeq1d 3078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ⊊ 𝑓 → ((𝑓 ∩ ℎ) ≠ ∅ ↔ ℎ ≠ ∅))
350	349	biimpar 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∩ ℎ) ≠ ∅)
351		disj4 4411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∩ ℎ) = ∅ ↔ ¬ (𝑓 ∖ ℎ) ⊊ 𝑓)
352	351	bicomi 226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑓 ∖ ℎ) ⊊ 𝑓 ↔ (𝑓 ∩ ℎ) = ∅)
353	352	necon1abii 3067	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∩ ℎ) ≠ ∅ ↔ (𝑓 ∖ ℎ) ⊊ 𝑓)
354	350, 353	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∖ ℎ) ⊊ 𝑓)
355	354	ad2antrl 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ∖ ℎ) ⊊ 𝑓)
356	128	difexi 5235	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∖ ℎ) ∈ V
357		psseq1 4067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ ℎ) ⊊ 𝑓))
358		xpeq1 5572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 × 𝑏) = ((𝑓 ∖ ℎ) × 𝑏))
359	358	pweqd 4561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ ℎ) × 𝑏))
360		pweq 4558	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ ℎ))
361	360	raleqdv 3418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑)))
362		f1eq2 6574	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ ℎ)–1-1→V))
363	362	rexbidv 3300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
364	361, 363	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
365	359, 364	raleqbidv 3404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
366	357, 365	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))))
367	356, 366	spcv 3609	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
368	241, 355, 367	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
369		imaeq1 5927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
370	369	breq2d 5081	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
371	370	ralbidv 3200	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
372		pweq 4558	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
373	372	rexeqdv 3419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
374	371, 373	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)))
375	374	rspcva 3624	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
376	344, 368, 375	sylancr 589	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
377	336, 376	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)
378		f1eq1 6573	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑗 → (𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ 𝑗:(𝑓 ∖ ℎ)–1-1→V))
379	378	cbvrexvw 3453	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
380	377, 379	sylib 220	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
381		elpwi 4551	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ (𝑔 ↾ ℎ))
382		resss 5881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ↾ ℎ) ⊆ 𝑔
383	381, 382	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ 𝑔)
384	383	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖 ⊆ 𝑔)
385	384	ad2antlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖 ⊆ 𝑔)
386		elpwi 4551	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
387		inss1 4208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ 𝑔
388	386, 387	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ 𝑔)
389	388	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗 ⊆ 𝑔)
390	385, 389	unssd 4165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ⊆ 𝑔)
391	45	elpw2 5251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ↔ (𝑖 ∪ 𝑗) ⊆ 𝑔)
392	390, 391	sylibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ∈ 𝒫 𝑔)
393		f1f1orn 6629	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖:ℎ–1-1→V → 𝑖:ℎ–1-1-onto→ran 𝑖)
394	393	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖:ℎ–1-1-onto→ran 𝑖)
395	394	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖:ℎ–1-1-onto→ran 𝑖)
396		f1f1orn 6629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗:(𝑓 ∖ ℎ)–1-1→V → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
397	396	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
398		disjdif 4424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∩ (𝑓 ∖ ℎ)) = ∅
399	398	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∩ (𝑓 ∖ ℎ)) = ∅)
400		rnss 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ⊆ (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
401	381, 400	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
402		df-ima 5571	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔 “ ℎ) = ran (𝑔 ↾ ℎ)
403	401, 402	sseqtrrdi 4021	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ (𝑔 “ ℎ))
404	403	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → ran 𝑖 ⊆ (𝑔 “ ℎ))
405	404	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑖 ⊆ (𝑔 “ ℎ))
406		incom 4181	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔 “ ℎ))
407	386, 337	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
408		rnss 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
409	407, 408	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
410		rnxpss 6032	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ (𝑏 ∖ (𝑔 “ ℎ))
411	409, 410	sstrdi 3982	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
412	411	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
413		incom 4181	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ((𝑔 “ ℎ) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
414		disjdif 4424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 “ ℎ) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ∅
415	413, 414	eqtri 2847	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅
416		ssdisj 4412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)) ∧ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
417	412, 415, 416	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
418	406, 417	syl5eq 2871	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅)
419		ssdisj 4412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑖 ⊆ (𝑔 “ ℎ) ∧ ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
420	405, 418, 419	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
421		f1oun 6637	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖:ℎ–1-1-onto→ran 𝑖 ∧ 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗) ∧ ((ℎ ∩ (𝑓 ∖ ℎ)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
422	395, 397, 399, 420, 421	syl22anc 836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
423		undif 4433	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
424	423	biimpi 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
425	424	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
426	425	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
427	426	f1oeq2d 6614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
428	422, 427	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
429		f1of1 6617	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
430	428, 429	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
431		ssv 3994	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑖 ∪ ran 𝑗) ⊆ V
432		f1ss 6583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
433	430, 431, 432	sylancl 588	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
434		f1eq1 6573	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖 ∪ 𝑗) → (𝑒:𝑓–1-1→V ↔ (𝑖 ∪ 𝑗):𝑓–1-1→V))
435	434	rspcev 3626	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ∧ (𝑖 ∪ 𝑗):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
436	392, 433, 435	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
437	436	rexlimdvaa 3288	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
438	437	rexlimdvaa 3288	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
439	254, 223, 438	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
440	274, 380, 439	mp2d 49	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
441	440	ex 415	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
442	441	exlimdv 1933	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
443	442	imp 409	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
444	220, 443	sylan2br 596	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
445	219, 444	pm2.61dan 811	. . . . . . . 8 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
446	445	exp32 423	. . . . . . 7 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
447	446	ralrimiv 3184	. . . . . 6 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
448		imaeq1 5927	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 “ 𝑑) = (𝑐 “ 𝑑))
449	448	breq2d 5081	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ (𝑐 “ 𝑑)))
450	449	ralbidv 3200	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
451		pweq 4558	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
452	451	rexeqdv 3419	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
453	450, 452	imbi12d 347	. . . . . . 7 ⊢ (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
454	453	cbvralvw 3452	. . . . . 6 ⊢ (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
455	447, 454	sylib 220	. . . . 5 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
456	455	exp31 422	. . . 4 ⊢ (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
457	456	a2d 29	. . 3 ⊢ (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
458	22, 457	syl5bi 244	. 2 ⊢ (𝑓 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
459	9, 18, 458	findcard3 8764	1 ⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534   = wceq 1536  ∃wex 1779   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  ∃wrex 3142  Vcvv 3497   ∖ cdif 3936   ∪ cun 3937   ∩ cin 3938   ⊆ wss 3939   ⊊ wpss 3940  ∅c0 4294  𝒫 cpw 4542  {csn 4570  ⟨cop 4576   class class class wbr 5069   × cxp 5556  ran crn 5559   ↾ cres 5560   “ cima 5561  –1-1→wf1 6355  –1-1-onto→wf1o 6357   ≈ cen 8509   ≼ cdom 8510   ≺ csdm 8511  Fincfn 8512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-om 7584  df-1o 8105  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-fin 8516

This theorem is referenced by:  marypha1  8901